\documentclass{article}
%\usepackage[latin9]{inputenc}
\usepackage{hevea}
\usepackage{fullpage}
\usepackage{alltt}
\usepackage{xspace}
\usepackage[pdfborder={0 0 0}]{hyperref}
\usepackage{listings}
\usepackage[usenames,dvipsnames]{color}
\usepackage[T1]{fontenc}
\usepackage{multirow}

\lstset{basicstyle=\ttfamily,numbers=left, numberstyle=\tiny, stepnumber=1, numbersep=5pt,language=C,commentstyle=\color{OliveGreen},keywordstyle=\color{blue},stringstyle=\color{BrickRed}}

%
% You must prefix the +/- lines of
% cocci files with @+/@- respectively.
% This will enable the automatic coloration.
%
% Note: You need at least the following version of hevea
% http://hevea.inria.fr/distri/unstable/hevea-2008-12-17.tar.gz
%
\ifhevea % For HTML generation
\lstdefinelanguage{Cocci}{
morekeywords={idexpression,expression,statement,identifier,type,
parameter,list,when,strict,any,forall,local,position,typedef},
keywordstyle=\color{OliveGreen}\bfseries,
sensitive=false,
moredelim=[is][\color{blue}]{@M}{@M},
moredelim=[il][\color{OliveGreen}]{@+},
moredelim=[il][\color{BrickRed}]{@-}}

\lstdefinelanguage{PatchC}[ANSI]{C}{
stringstyle=\color{black},
moredelim=[il][\color{OliveGreen}]{@+},
moredelim=[il][\color{BrickRed}]{@-},
moredelim=[il][\color{Plum}]{@M}}

\else % For DVI/PS/PDF generation
\lstdefinelanguage{Cocci}{
morekeywords={idexpression,expression,statement,identifier,type,
parameter,list,when,strict,any,forall,local,position,typedef},
keywordstyle=\color{OliveGreen}\bfseries,
sensitive=false,
moredelim=*[is][\color{blue}]{@M}{@M},
moredelim=[il][\color{OliveGreen}]{@+},
moredelim=[il][\color{BrickRed}]{@-}}

\lstdefinelanguage{PatchC}[ANSI]{C}{
stringstyle=\color{black},
moredelim=[il][\color{OliveGreen}]{@+},
moredelim=[il][\color{BrickRed}]{@-},
moredelim=[il][\color{Plum}]{@M}}
\fi

\newif\iflanguagestyle
\languagestylefalse
\input{grammar}

\newcommand{\sizecodebis}[0]{\scriptsize}

\newcommand{\mita}[1]{\mbox{\it{{#1}}}}
\newcommand{\mtt}[1]{\mbox{\tt{{#1}}}}
\newcommand{\msf}[1]{\mbox{\sf{{#1}}}}
\newcommand{\stt}[1]{\mbox{\scriptsize\tt{{#1}}}}
\newcommand{\ssf}[1]{\mbox{\scriptsize\sf{{#1}}}}
\newcommand{\sita}[1]{\mbox{\scriptsize\it{{#1}}}}
\newcommand{\mrm}[1]{\mbox{\rm{{#1}}}}
\newcommand{\mth}[1]{\({#1}\)}
\newcommand{\entails}[2]{\begin{array}{@{}c@{}}{#1}\\\hline{#2}\end{array}}
\newcommand{\ttlb}{\mbox{\tt \char'173}}
\newcommand{\ttrb}{\mbox{\tt \char'175}}
\newcommand{\ttmid}{\mbox{\tt \char'174}}
\newcommand{\tttld}{\mbox{\tt \char'176}}

\newcommand{\fixme}[1]{{\color{red} #1}}

\ifhevea
\newcommand{\phantom}{}
\newcommand{\air}{   }
\else
\newcommand{\air}{\phantom{xxx}}
\fi

\title{The SmPL Grammar (version 0.1.4)}
\author{Research group on Coccinelle}
\date{\today}

\begin{document}
\maketitle

%\section{The SmPL Grammar}

% This section presents the SmPL grammar.  This definition follows closely
% our implementation using the Menhir parser generator \cite{menhir}.

This document presents the grammar of the SmPL language used by the
\href{http://www.emn.fr/x-info/coccinelle}{Coccinelle tool}.  For the most
part, the grammar is written using standard notation.  In some rules,
however, the left-hand side is in all uppercase letters.  These are
macros, which take one or more grammar rule right-hand-sides as
arguments.  The grammar also uses some unspecified nonterminals, such
as {\sf id}, {\sf const}, etc.  These refer to the sets suggested by
the name, {\em i.e.}, {\sf id} refers to the set of possible
C-language identifiers, while {\sf const} refers to the set of
possible C-language constants.  \ifhevea A PDF version of this
documentation is available at
\url{http://www.emn.fr/x-info/coccinelle/docs/cocci_syntax.pdf}.\else
A HTML version of this documentation is available online at
\url{http://www.emn.fr/x-info/coccinelle/docs/cocci_syntax.html}. \fi

%% \ifhevea A PDF
%% version of this documentation is available at
%% \url{http://localhost:8080/coccinelle/cocci_syntax.pdf}.\else A HTML
%% version of this documentation is available online at
%% \url{http://localhost:8080/coccinelle/cocci_syntax.html}. \fi

\section{Program}

\begin{grammar}
  \RULE{\rt{program}}
  \CASE{\any{\NT{include\_cocci}} \some{\NT{changeset}}}

  \RULE{\rt{include\_cocci}}
  \CASE{using \NT{string}}
  \CASE{using \NT{pathToIsoFile}}

  \RULE{\rt{changeset}}
  \CASE{\NT{metavariables} \NT{transformation}}
%  \CASE{\NT{metavariables} \ANY{--- filename +++ filename} \NT{transformation}}

\end{grammar}

% Between the metavariables and the transformation rule, there can be a
% specification of constraints on the names of the old and new files,
% analogous to the filename specifications in the standard patch syntax.
% (see Figure \ref{scsiglue_patch}).

\section{Metavariables}

The \NT{rulename} portion of the metavariable declaration can specify
properties of a rule such as its name, the names of the rules that it
depends on, the isomorphisms to be used in processing the rule, and whether
quantification over paths should be universal or existential.  The optional
annotation {\tt expression} indicates that the pattern is to be considered
as matching an expression, and thus can be used to avoid some parsing
problems.

The \NT{metadecl} portion of the metavariable declaration defines various
types of metavariables that will be used for matching in the transformation
section.

\begin{grammar}
  \RULE{\rt{metavariables}}
  \CASE{@@ \any{\NT{metadecl}} @@}
  \CASE{@ \NT{rulename} @ \any{\NT{metadecl}} @@}

  \RULE{\rt{rulename}}
  \CASE{\T{id} \OPT{extends \T{id}} \OPT{depends on \NT{dep}} \opt{\NT{iso}}
    \opt{\NT{disable-iso}} \opt{\NT{exists}} \opt{expression}}
  \CASE{script:\T{language} \OPT{depends on \NT{dep}}}

  \RULE{\rt{dep}}
  \CASE{\NT{pnrule}}
  \CASE{\NT{dep} \&\& \NT{dep}}
  \CASE{\NT{dep} || \NT{dep}}

  \RULE{\rt{pnrule}}
  \CASE{\T{id}}
  \CASE{!\T{id}}
  \CASE{ever \T{id}}
  \CASE{never \T{id}}
  \CASE{(\NT{dep})}

  \RULE{\rt{iso}}
  \CASE{using \NT{string} \ANY{, \NT{string}}}

  \RULE{\rt{disable-iso}}
  \CASE{disable \NT{COMMA\_LIST}\mth{(}\T{id}\mth{)}}

  \RULE{\rt{exists}}
  \CASE{exists}
  \CASE{forall}
%  \CASE{\opt{reverse} forall}

  \RULE{\rt{COMMA\_LIST}\mth{(}\rt{elem}\mth{)}}
  \CASE{\NT{elem} \ANY{, \NT{elem}}}
\end{grammar}

The keyword \NT{disable-iso} is normally used with the names of
isomorphisms defined in standard.iso or whatever isomorphism file has been
included.  There are, however, some other isomorphisms that are built into
the implementation of Coccinelle and that can be disabled as well.  Their
names are given below.  In each case, the text descibes the standard
behavior.  Using \NT{disable-iso} with the given name disables this behavior.

\begin{itemize}
\item \KW{optional\_storage}: A SmPL function definition that does not
  specify any visibility (i.e., static or extern), or a SmPL variable
  declaration that does not specify any storage (i.e., auto, static,
  register, or extern), matches a function declaration or variable
  declaration with any visibility or storage, respectively.
\item \KW{optional\_qualifier}: This is similar to \KW{optional\_storage},
  except that here is it the qualifier (i.e., const or volatile) that does
  not have to be specified in the SmPL code, but may be present in the C code.
\item \KW{value\_format}: Integers in various formats, e.g., 1 and 0x1, are
  considered to be equivalent in the matching process.
\item \KW{comm\_assoc}: An expression of the form \NT{exp} \NT{bin\_op}
  \KW{...}, where \NT{bin\_op} is commutative and associative, is
  considered to match any top-level sequence of \NT{bin\_op} operators
  containing \NT{exp} as the top-level argument.
\end{itemize}

The possible types of metavariable declarations are defined by the grammar
rule below.  Metavariables should occur at least once in the transformation
immediately following their declaration.  Fresh metavariables must only be
used in {\tt +} code.  These properties are not expressed in the grammar,
but are checked by a subsequent analysis.  The metavariables are designated
according to the kind of terms they can match, such as a statement, an
identifier, or an expression.  An expression metavariable can be further
constrained by its type.

\begin{grammar}
  \RULE{\rt{metadecl}}
  \CASE{fresh identifier \NT{ids} ;}
  \CASE{identifier \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{parameter \opt{list} \NT{ids} ;}
  \CASE{parameter list [ \NT{id} ] \NT{ids} ;}
  \CASE{type \NT{ids} ;}
  \CASE{statement \opt{list} \NT{ids} ;}
  \CASE{typedef \NT{ids} ;}
  \CASE{declarer name \NT{ids} ;}
%  \CASE{\opt{local} function \NT{pmid\_with\_not\_eq\_list} ;}
  \CASE{declarer \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{iterator name \NT{ids} ;}
  \CASE{iterator \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
%  \CASE{error \NT{pmid\_with\_not\_eq\_list} ; }
  \CASE{\opt{local} idexpression \opt{\NT{ctype}} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{\opt{local} idexpression \OPT{\ttlb \NT{ctypes}\ttrb~\any{*}} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{\opt{local} idexpression \some{*} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{expression list \NT{ids} ;}
  \CASE{expression \some{*} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{expression \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_ceq}\mth{)} ;}
  \CASE{expression list [ ident ] \NT{ids} ;}
  \CASE{\NT{ctype} [ ] \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{\NT{ctype} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_ceq}\mth{)} ;}
  \CASE{\ttlb \NT{ctypes}\ttrb~\any{*} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_ceq}\mth{)} ;}
  \CASE{\ttlb \NT{ctypes}\ttrb~\any{*} [ ] \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{constant \opt{\NT{ctype}} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{constant \OPT{\ttlb \NT{ctypes}\ttrb~\any{*}} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq}\mth{)} ;}
  \CASE{position \opt{any} \NT{COMMA\_LIST}\mth{(}\NT{pmid\_with\_not\_eq\_mid}\mth{)} ;}
\end{grammar}

\begin{grammar}
  \RULE{\rt{ids}}
  \CASE{\NT{COMMA\_LIST}\mth{(}\NT{pmid}\mth{)}}

  \RULE{\rt{pmid}}
  \CASE{\T{id}}
  \CASE{\NT{mid}}
%   \CASE{list}
%   \CASE{error}
%   \CASE{type}

  \RULE{\rt{mid}}  \CASE{\T{rulename\_id}.\T{id}}

  \RULE{\rt{pmid\_with\_not\_eq}}
  \CASE{\NT{pmid} \OPT{!= \T{id}}}
  \CASE{\NT{pmid} \OPT{!= \ttlb~\NT{COMMA\_LIST}\mth{(}\T{id}\mth{)} \ttrb}}

  \RULE{\rt{pmid\_with\_not\_ceq}}
  \CASE{\NT{pmid} \OPT{!= \NT{id\_or\_cst}}}
  \CASE{\NT{pmid} \OPT{!= \ttlb~\NT{COMMA\_LIST}\mth{(}\NT{id\_or\_cst}\mth{)} \ttrb}}

  \RULE{\rt{id\_or\_cst}}
  \CASE{\T{id}}
  \CASE{\T{integer}}

  \RULE{\rt{pmid\_with\_not\_eq\_mid}}
  \CASE{\NT{pmid} \OPT{!= \NT{mid}}}
  \CASE{\NT{pmid} \OPT{!= \ttlb~\NT{COMMA\_LIST}\mth{(}\NT{mid}\mth{)} \ttrb}}
\end{grammar}

Subsequently, we refer to arbitrary metavariables as
\mth{\msf{metaid}^{\mbox{\scriptsize{\it{ty}}}}}, where {\it{ty}}
indicates the {\it metakind} used in the declaration of the variable.
For example, \mth{\msf{metaid}^{\ssf{Type}}} refers to a metavariable
that was declared using \texttt{type} and stands for any type.

The \NT{ctype} and \NT{ctypes} nonterminals are used by both the grammar of
metavariable declarations and the grammar of transformations, and are
defined on page~\pageref{types}.

\section{Transformation}

The transformation specification essentially has the form of C code,
except that lines to remove are annotated with \verb+-+ in the first
column, and lines to add are annotated with \verb-+-.  A
transformation specification can also use {\em dots}, ``\verb-...-'',
describing an arbitrary sequence of function arguments or instructions
within a control-flow path.  Dots may be modified with a {\tt when}
clause, indicating a pattern that should not occur anywhere within the
matched sequence.  Finally, a transformation can specify a disjunction
of patterns, of the form \mtt{( \mth{\mita{pat}_1} | \mita{\ldots} |
  \mth{\mita{pat}_n} )} where each \texttt{(}, \texttt{|} or
\texttt{)} is in column 0 or preceded by \texttt{\textbackslash}.

The grammar that we present for the transformation is not actually the
grammar of the SmPL code that can be written by the programmer, but is
instead the grammar of the slice of this consisting of the {\tt -}
annotated and the unannotated code (the context of the transformed lines),
or the {\tt +} annotated code and the unannotated code.  For example, for
parsing purposes, the following transformation
%presented in Section \ref{sec:seq2}
is split into the two variants shown below and each is parsed
separately.

\begin{center}
\begin{tabular}{c}
\begin{lstlisting}[language=Cocci]
  proc_info_func(...) {
    <...
@--    hostno
@++    hostptr->host_no
    ...>
 }
\end{lstlisting}\\
\end{tabular}
\end{center}

{%\sizecodebis
\begin{center}
\begin{tabular}{p{5cm}p{3cm}p{5cm}}
\begin{lstlisting}[language=Cocci]
  proc_info_func(...) {
    <...
@--    hostno
    ...>
 }
\end{lstlisting}
&&
\begin{lstlisting}[language=Cocci]
  proc_info_func(...) {
    <...
@++    hostptr->host_no
    ...>
 }
\end{lstlisting}
\end{tabular}
\end{center}
}

\noindent
Requiring that both slices parse correctly ensures that the rule matches
syntactically valid C code and that it produces syntactically valid C code.
The generated parse trees are then merged for use in the subsequent
matching and transformation process.

The grammar for the minus or plus slice of a transformation is as follows:

\begin{grammar}

  \RULE{\rt{transformation}}
  \CASE{\some{\NT{include}}}
  \CASE{\NT{OPTDOTSEQ}\mth{(}\NT{expr}, \NT{when}\mth{)}}
  \CASE{\NT{OPTDOTSEQ}\mth{(}\some{\NT{decl\_stmt}}, \NT{when}\mth{)}}
  \CASE{\NT{OPTDOTSEQ}\mth{(}\NT{fundecl}, \NT{when}\mth{)}}

  \RULE{\rt{include}}
  \CASE{\#include \T{include\_string}}

%  \RULE{\rt{fun\_decl\_stmt}}
%  \CASE{\NT{decl\_stmt}}
%  \CASE{\NT{fundecl}}

%  \CASE{\NT{ctype}}
%  \CASE{\ttlb \NT{initialize\_list} \ttrb}
%  \CASE{\NT{toplevel\_seq\_start\_after\_dots\_init}}
%
%  \RULE{\rt{toplevel\_seq\_start\_after\_dots\_init}}
%  \CASE{\NT{stmt\_dots} \NT{toplevel\_after\_dots}}
%  \CASE{\NT{expr} \opt{\NT{toplevel\_after\_exp}}}
%  \CASE{\NT{decl\_stmt\_expr} \opt{\NT{toplevel\_after\_stmt}}}
%
%  \RULE{\rt{stmt\_dots}}
%  \CASE{... \any{\NT{when}}}
%  \CASE{<... \any{\NT{when}} \NT{nest\_after\_dots} ...>}
%  \CASE{<+... \any{\NT{when}} \NT{nest\_after\_dots} ...+>}

  \RULE{\rt{when}}
  \CASE{when != \NT{when\_code}}
  \CASE{when = \NT{rule\_elem\_stmt}}
  \CASE{when \NT{COMMA\_LIST}\mth{(}\NT{any\_strict}\mth{)}}
  \CASE{when true != \NT{expr}}
  \CASE{when false != \NT{expr}}

  \RULE{\rt{when\_code}}
  \CASE{\NT{OPTDOTSEQ}\mth{(}\some{\NT{decl\_stmt}}, \NT{when}\mth{)}}
  \CASE{\NT{OPTDOTSEQ}\mth{(}\NT{expr}, \NT{when}\mth{)}}

  \RULE{\rt{rule\_elem\_stmt}}
  \CASE{\NT{one\_decl}}
  \CASE{\NT{expr};}
  \CASE{return \opt{\NT{expr}};}
  \CASE{break;}
  \CASE{continue;}
  \CASE{\bs(\NT{rule\_elem\_stmt} \SOME{\bs| \NT{rule\_elem\_stmt}}\bs)}

  \RULE{\rt{any\_strict}}
  \CASE{any}
  \CASE{strict}
  \CASE{forall}
  \CASE{exists}

%  \RULE{\rt{nest\_after\_dots}}
%  \CASE{\NT{decl\_stmt\_exp} \opt{\NT{nest\_after\_stmt}}}
%  \CASE{\opt{\NT{exp}} \opt{\NT{nest\_after\_exp}}}
%
%  \RULE{\rt{nest\_after\_stmt}}
%  \CASE{\NT{stmt\_dots} \NT{nest\_after\_dots}}
%  \CASE{\NT{decl\_stmt} \opt{\NT{nest\_after\_stmt}}}
%
%  \RULE{\rt{nest\_after\_exp}}
%  \CASE{\NT{stmt\_dots} \NT{nest\_after\_dots}}
%
%  \RULE{\rt{toplevel\_after\_dots}}
%  \CASE{\opt{\NT{toplevel\_after\_exp}}}
%  \CASE{\NT{exp} \opt{\NT{toplevel\_after\_exp}}}
%  \CASE{\NT{decl\_stmt\_expr} \NT{toplevel\_after\_stmt}}
%
%  \RULE{\rt{toplevel\_after\_exp}}
%  \CASE{\NT{stmt\_dots} \opt{\NT{toplevel\_after\_dots}}}
%
%  \RULE{\rt{decl\_stmt\_expr}}
%  \CASE{TMetaStmList$^\ddag$}
%  \CASE{\NT{decl\_var}}
%  \CASE{\NT{stmt}}
%  \CASE{(\NT{stmt\_seq} \ANY{| \NT{stmt\_seq}})}
%
%  \RULE{\rt{toplevel\_after\_stmt}}
%  \CASE{\NT{stmt\_dots} \opt{\NT{toplevel\_after\_dots}}}
%  \CASE{\NT{decl\_stmt} \NT{toplevel\_after\_stmt}}

\end{grammar}

\begin{grammar}
  \RULE{\rt{OPTDOTSEQ}\mth{(}\rt{grammar\_ds}, \rt{when\_ds}\mth{)}}
  \CASE{}\multicolumn{3}{r}{\hspace{1cm}
  \KW{\opt{... \opt{\NT{when\_ds}}} \NT{grammar\_ds}
    \ANY{... \opt{\NT{when\_ds}} \NT{grammar\_ds}}
    \opt{... \opt{\NT{when\_ds}}}}
  }

%  \CASE{\opt{... \opt{\NT{when\_ds}}} \NT{grammar}
%    \ANY{... \opt{\NT{when\_ds}} \NT{grammar}}
%    \opt{... \opt{\NT{when\_ds}}}}
%  \CASE{<... \any{\NT{when\_ds}} \NT{grammar} ...>}
%  \CASE{<+... \any{\NT{when\_ds}} \NT{grammar} ...+>}

\end{grammar}

\noindent
Lines may be annotated with an element of the set $\{\mtt{-}, \mtt{+},
\mtt{*}\}$ or the singleton $\mtt{?}$, or one of each set. \mtt{?}
represents at most one match of the given pattern. \mtt{*} is used for
semantic match, \emph{i.e.}, a pattern that highlights the fragments
annotated with \mtt{*}, but does not perform any modification of the
matched code. \mtt{*} cannot be mixed with \mtt{-} and \mtt{+}.  There are
some constraints on the use of these annotations:
\begin{itemize}
\item Dots, {\em i.e.} \texttt{...}, cannot occur on a line marked
  \texttt{+}.
\item Nested dots, {\em i.e.}, dots enclosed in {\tt <} and {\tt >}, cannot
  occur on a line with any marking.
\end{itemize}

Each element of a disjunction must be a proper term like an
expression, a statement, an identifier or a declaration. Thus, the
rule on the left below is not a syntaxically correct SmPL rule. One may
use the rule on the right instead.

\begin{center}
  \begin{tabular}{l@{\hspace{5cm}}r}
\begin{lstlisting}[language=Cocci]
@@
type T;
T b;
@@

(
 writeb(...,
|
 readb(
)
@--(T)
 b)
\end{lstlisting}
    &
\begin{lstlisting}[language=Cocci]
@@
type T;
T b;
@@

(
read
|
write
)
 (...,
@-- (T)
  b)
\end{lstlisting}
    \\
  \end{tabular}
\end{center}

\section{Types}
\label{types}

\begin{grammar}

  \RULE{\rt{ctypes}}
  \CASE{\NT{COMMA\_LIST}\mth{(}\NT{ctype}\mth{)}}

  \RULE{\rt{ctype}}
  \CASE{\opt{\NT{const\_vol}} \NT{generic\_ctype} \any{*}}
  \CASE{\opt{\NT{const\_vol}} void \some{*}}
  \CASE{(\NT{ctype} \ANY{| \NT{ctype}})}

  \RULE{\rt{const\_vol}}
  \CASE{const}
  \CASE{volatile}

  \RULE{\rt{generic\_ctype}}
  \CASE{\NT{ctype\_qualif}}
  \CASE{\opt{\NT{ctype\_qualif}} char}
  \CASE{\opt{\NT{ctype\_qualif}} short}
  \CASE{\opt{\NT{ctype\_qualif}} int}
  \CASE{\opt{\NT{ctype\_qualif}} long}
  \CASE{\opt{\NT{ctype\_qualif}} long long}
  \CASE{double}
  \CASE{float}
  \CASE{\OPT{struct\OR union} \T{id} \OPT{\{ \any{\NT{struct\_decl\_list}} \}}}

  \RULE{\rt{ctype\_qualif}}
  \CASE{unsigned}
  \CASE{signed}

  \RULE{\rt{struct\_decl\_list}}
  \CASE{\NT{struct\_decl\_list\_start}}

  \RULE{\rt{struct\_decl\_list\_start}}
  \CASE{\NT{struct\_decl}}
  \CASE{\NT{struct\_decl} \NT{struct\_decl\_list\_start}}
  \CASE{... \opt{when != \NT{struct\_decl}}$^\dag$ \opt{\NT{continue\_struct\_decl\_list}}}

  \RULE{\rt{continue\_struct\_decl\_list}}
  \CASE{\NT{struct\_decl} \NT{struct\_decl\_list\_start}}
  \CASE{\NT{struct\_decl}}

  \RULE{\rt{struct\_decl}}
  \CASE{\NT{ctype} \NT{d\_ident};}
  \CASE{\NT{fn\_ctype} (* \NT{d\_ident}) (\NT{PARAMSEQ}\mth{(}\NT{name\_opt\_decl}, \mth{\varepsilon)});)}
  \CASE{\opt{\NT{const\_vol}} \T{id} \NT{d\_ident};}

  \RULE{\rt{d\_ident}}
  \CASE{\NT{id} \any{[\opt{\NT{expr}}]}}

  \RULE{\rt{fn\_ctype}}
  \CASE{\NT{generic\_ctype} \any{*}}
  \CASE{void \any{*}}

  \RULE{\rt{name\_opt\_decl}}
  \CASE{\NT{decl}}
  \CASE{\NT{ctype}}
  \CASE{\NT{fn\_ctype}}
\end{grammar}

$^\dag$ The optional \texttt{when} construct ends at the end of the line.

\section{Function declarations}

\begin{grammar}

  \RULE{\rt{fundecl}}
  \CASE{\opt{\NT{fn\_ctype}} \any{\NT{funinfo}} \NT{funid}
    (\opt{\NT{PARAMSEQ}\mth{(}\NT{param}, \mth{\varepsilon)}})
    \ttlb~\opt{\NT{stmt\_seq}} \ttrb}

  \RULE{\rt{funproto}}
  \CASE{\opt{\NT{fn\_ctype}} \any{\NT{funinfo}} \NT{funid}
    (\opt{\NT{PARAMSEQ}\mth{(}\NT{param}, \mth{\varepsilon)}});}

  \RULE{\rt{funinfo}}
  \CASE{inline}
  \CASE{\NT{storage}}
%   \CASE{\NT{attr}}

  \RULE{\rt{storage}}
  \CASE{static}
  \CASE{auto}
  \CASE{register}
  \CASE{extern}

  \RULE{\rt{funid}}
  \CASE{\T{id}}
  \CASE{\mth{\T{metaid}^{\ssf{Id}}}}
%   \CASE{\mth{\T{metaid}^{\ssf{Func}}}}
%   \CASE{\mth{\T{metaid}^{\ssf{LocalFunc}}}}

  \RULE{\rt{param}}
  \CASE{\NT{type} \T{id}}
  \CASE{\mth{\T{metaid}^{\ssf{Param}}}}
  \CASE{\mth{\T{metaid}^{\ssf{ParamList}}}}

  \RULE{\rt{decl}}
  \CASE{\NT{ctype} \NT{id}}
  \CASE{\NT{fn\_ctype} (* \NT{id}) (\NT{PARAMSEQ}\mth{(}\NT{name\_opt\_decl}, \mth{\varepsilon)})}
  \CASE{void}
  \CASE{\mth{\T{metaid}^{\ssf{Param}}}}
\end{grammar}

\begin{grammar}
  \RULE{\rt{PARAMSEQ}\mth{(}\rt{gram\_p}, \rt{when\_p}\mth{)}}
  \CASE{\NT{COMMA\_LIST}\mth{(}\NT{gram\_p} \OR \ldots \opt{\NT{when\_p}}\mth{)}}
\end{grammar}

%\newpage

\section{Declarations}

\begin{grammar}
  \RULE{\rt{decl\_var}}
%  \CASE{\NT{type} \opt{\NT{id} \opt{[\opt{\NT{dot\_expr}}]}
%      \ANY{, \NT{id} \opt{[ \opt{\NT{dot\_expr}}]}}};}
  \CASE{\NT{common\_decl}}
  \CASE{\opt{\NT{storage}} \NT{ctype} \NT{COMMA\_LIST}\mth{(}\NT{d\_ident}\mth{)} ;}
  \CASE{\opt{\NT{storage}} \opt{\NT{const\_vol}} \T{id} \NT{COMMA\_LIST}\mth{(}\NT{d\_ident}\mth{)} ;}
  \CASE{\opt{\NT{storage}} \NT{fn\_ctype} ( * \NT{d\_ident} ) ( \NT{PARAMSEQ}\mth{(}\NT{name\_opt\_decl}, \mth{\varepsilon)} ) = \NT{initialize} ;}
  \CASE{typedef \NT{ctype} \NT{typedef\_ident} ;}

  \RULE{\rt{one\_decl}}
  \CASE{\NT{common\_decl}}
  \CASE{\opt{\NT{storage}} \NT{ctype} \NT{id};}
%  \CASE{\NT{storage} \NT{ctype} \NT{id} \opt{[\opt{\NT{dot\\_expr}}]} = \NT{nest\\_expr};}
  \CASE{\opt{\NT{storage}} \opt{\NT{const\_vol}} \T{id} \NT{d\_ident} ;}

  \RULE{\rt{common\_decl}}
  \CASE{\NT{ctype};}
  \CASE{\NT{funproto}}
  \CASE{\opt{\NT{storage}} \NT{ctype} \NT{d\_ident} = \NT{initialize} ;}
  \CASE{\opt{\NT{storage}} \opt{\NT{const\_vol}} \T{id} \NT{d\_ident} = \NT{initialize} ;}
  \CASE{\opt{\NT{storage}} \NT{fn\_ctype} ( * \NT{d\_ident} ) ( \NT{PARAMSEQ}\mth{(}\NT{name\_opt\_decl}, \mth{\varepsilon)} ) ;}
  \CASE{\NT{decl\_ident} ( \OPT{\NT{COMMA\_LIST}\mth{(}\NT{expr}\mth{)}} ) ;}

  \RULE{\rt{initialize}}
  \CASE{\NT{dot\_expr}}
  \CASE{\ttlb~\opt{\NT{COMMA\_LIST}\mth{(}\NT{dot\_expr}\mth{)}}~\ttrb}

  \RULE{\rt{decl\_ident}}
  \CASE{\T{DeclarerId}}
  \CASE{\mth{\T{metaid}^{\ssf{Declarer}}}}
\end{grammar}

\section{Statements}

The first rule {\em statement} describes the various forms of a statement.
The remaining rules implement the constraints that are sensitive to the
context in which the statement occurs: {\em single\_statement} for a
context in which only one statement is allowed, and {\em decl\_statement}
for a context in which a declaration, statement, or sequence thereof is
allowed.

\begin{grammar}
  \RULE{\rt{stmt}}
  \CASE{\NT{include}}
  \CASE{\mth{\T{metaid}^{\ssf{Stmt}}}}
  \CASE{\NT{expr};}
  \CASE{if (\NT{dot\_expr}) \NT{single\_stmt} \opt{else \NT{single\_stmt}}}
  \CASE{for (\opt{\NT{dot\_expr}}; \opt{\NT{dot\_expr}}; \opt{\NT{dot\_expr}})
    \NT{single\_stmt}}
  \CASE{while (\NT{dot\_expr}) \NT{single\_stmt}}
  \CASE{do \NT{single\_stmt} while (\NT{dot\_expr});}
  \CASE{\NT{iter\_ident} (\any{\NT{dot\_expr}}) \NT{single\_stmt}}
  \CASE{switch (\opt{\NT{dot\_expr}}) \ttlb \any{\NT{case\_line}} \ttrb}
  \CASE{return \opt{\NT{dot\_expr}};}
  \CASE{\ttlb~\opt{\NT{stmt\_seq}} \ttrb}
  \CASE{\NT{NEST}\mth{(}\some{\NT{decl\_stmt}}, \NT{when}\mth{)}}
  \CASE{\NT{NEST}\mth{(}\NT{expr}, \NT{when}\mth{)}}
  \CASE{break;}
  \CASE{continue;}
  \CASE{\NT{id}:}
  \CASE{goto \NT{id};}
  \CASE{\ttlb \NT{stmt\_seq} \ttrb}

  \RULE{\rt{single\_stmt}}
  \CASE{\NT{stmt}}
  \CASE{\NT{OR}\mth{(}\NT{stmt}\mth{)}}

  \RULE{\rt{decl\_stmt}}
  \CASE{\mth{\T{metaid}^{\ssf{StmtList}}}}
  \CASE{\NT{decl\_var}}
  \CASE{\NT{stmt}}
  \CASE{\NT{OR}\mth{(}\NT{stmt\_seq}\mth{)}}

  \RULE{\rt{stmt\_seq}}
  \CASE{\any{\NT{decl\_stmt}}
    \opt{\NT{DOTSEQ}\mth{(}\some{\NT{decl\_stmt}},
      \NT{when}\mth{)} \any{\NT{decl\_stmt}}}}
  \CASE{\any{\NT{decl\_stmt}}
    \opt{\NT{DOTSEQ}\mth{(}\NT{expr},
      \NT{when}\mth{)} \any{\NT{decl\_stmt}}}}

  \RULE{\rt{case\_line}}
  \CASE{default :~\NT{stmt\_seq}}
  \CASE{case \NT{dot\_expr} :~\NT{stmt\_seq}}

  \RULE{\rt{iter\_ident}}
  \CASE{\T{IteratorId}}
  \CASE{\mth{\T{metaid}^{\ssf{Iterator}}}}
\end{grammar}

\begin{grammar}
  \RULE{\rt{OR}\mth{(}\rt{gram\_o}\mth{)}}
  \CASE{( \NT{gram\_o} \ANY{\ttmid \NT{gram\_o}})}

  \RULE{\rt{DOTSEQ}\mth{(}\rt{gram\_d}, \rt{when\_d}\mth{)}}
  \CASE{\ldots \opt{\NT{when\_d}} \ANY{\NT{gram\_d} \ldots \opt{\NT{when\_d}}}}

  \RULE{\rt{NEST}\mth{(}\rt{gram\_n}, \rt{when\_n}\mth{)}}
  \CASE{<\ldots \opt{\NT{when\_n}} \NT{gram\_n} \ANY{\ldots \opt{\NT{when\_n}} \NT{gram\_n}} \ldots>}
  \CASE{<+\ldots \opt{\NT{when\_n}} \NT{gram\_n} \ANY{\ldots \opt{\NT{when\_n}} \NT{gram\_n}} \ldots+>}
\end{grammar}

\noindent
OR is a macro that generates a disjunction of patterns.  The three
tokens \T{(}, \T{\ttmid}, and \T{)} must appear in the leftmost
column, to differentiate them from the parentheses and bit-or tokens
that can appear within expressions (and cannot appear in the leftmost
column). These token may also be preceded by \texttt{\bs}
when they are used in an other column.  These tokens are furthermore
different from (, \(\mid\), and ), which are part of the grammar
metalanguage.

\section{Expressions}

A nest or a single ellipsis is allowed in some expression contexts, and
causes ambiguity in others.  For example, in a sequence \mtt{\ldots
\mita{expr} \ldots}, the nonterminal \mita{expr} must be instantiated as an
explicit C-language expression, while in an array reference,
\mtt{\mth{\mita{expr}_1} \mtt{[} \mth{\mita{expr}_2} \mtt{]}}, the
nonterminal \mth{\mita{expr}_2}, because it is delimited by brackets, can
be also instantiated as \mtt{\ldots}, representing an arbitrary expression.  To
distinguish between the various possibilities, we define three nonterminals
for expressions: {\em expr} does not allow either top-level nests or
ellipses, {\em nest\_expr} allows a nest but not an ellipsis, and {\em
dot\_expr} allows both.  The EXPR macro is used to express these variants
in a concise way.

\begin{grammar}
  \RULE{\rt{expr}}
  \CASE{\NT{EXPR}\mth{(}\NT{expr}\mth{)}}

  \RULE{\rt{nest\_expr}}
  \CASE{\NT{EXPR}\mth{(}\NT{nest\_expr}\mth{)}}
  \CASE{\NT{NEST}\mth{(}\NT{nest\_expr}, \NT{exp\_whencode}\mth{)}}

  \RULE{\rt{dot\_expr}}
  \CASE{\NT{EXPR}\mth{(}\NT{dot\_expr}\mth{)}}
  \CASE{\NT{NEST}\mth{(}\NT{dot\_expr}, \NT{exp\_whencode}\mth{)}}
  \CASE{...~\opt{\NT{exp\_whencode}}}

  \RULE{\rt{EXPR}\mth{(}\rt{exp}\mth{)}}
  \CASE{\NT{exp} \NT{assign\_op} \NT{exp}}
  \CASE{\NT{exp}++}
  \CASE{\NT{exp}--}
  \CASE{\NT{unary\_op} \NT{exp}}
  \CASE{\NT{exp} \NT{bin\_op} \NT{exp}}
  \CASE{\NT{exp} ?~\NT{dot\_expr} :~\NT{exp}}
  \CASE{(\NT{type}) \NT{exp}}
  \CASE{\NT{exp} [\NT{dot\_expr}]}
  \CASE{\NT{exp} .~\NT{id}}
  \CASE{\NT{exp} -> \NT{id}}
  \CASE{\NT{exp}(\opt{\NT{PARAMSEQ}\mth{(}\NT{arg}, \NT{exp\_whencode}\mth{)}})}
  \CASE{\NT{id}}
%   \CASE{\mth{\T{metaid}^{\ssf{Func}}}}
%   \CASE{\mth{\T{metaid}^{\ssf{LocalFunc}}}}
  \CASE{\mth{\T{metaid}^{\ssf{Exp}}}}
%   \CASE{\mth{\T{metaid}^{\ssf{Err}}}}
  \CASE{\mth{\T{metaid}^{\ssf{Const}}}}
  \CASE{\NT{const}}
  \CASE{(\NT{dot\_expr})}
  \CASE{\NT{OR}\mth{(}\NT{exp}\mth{)}}

  \RULE{\rt{arg}}
  \CASE{\NT{nest\_expr}}
  \CASE{\mth{\T{metaid}^{\ssf{ExpList}}}}

  \RULE{\rt{exp\_whencode}}
  \CASE{when != \NT{expr}}

  \RULE{\rt{assign\_op}}
  \CASE{= \OR -= \OR += \OR *= \OR /= \OR \%=}
  \CASE{\&= \OR |= \OR \caret= \OR \lt\lt= \OR \gt\gt=}

  \RULE{\rt{bin\_op}}
  \CASE{* \OR / \OR \% \OR + \OR -}
  \CASE{\lt\lt \OR \gt\gt \OR \caret\xspace \OR \& \OR \ttmid}
  \CASE{< \OR > \OR <= \OR >= \OR == \OR != \OR \&\& \OR \ttmid\ttmid}

  \RULE{\rt{unary\_op}}
  \CASE{++ \OR -- \OR \& \OR * \OR + \OR - \OR !}

\end{grammar}

\section{Constant, Identifiers and Types for Transformations}

\begin{grammar}
  \RULE{\rt{const}}
  \CASE{\NT{string}}
  \CASE{[0-9]+}
  \CASE{\mth{\cdots}}

  \RULE{\rt{string}}
  \CASE{"\any{[\^{}"]}"}

  \RULE{\rt{id}}
  \CASE{\T{id} \OR \mth{\T{metaid}^{\ssf{Id}}}}

  \RULE{\rt{typedef\_ident}}
  \CASE{\T{id} \OR \mth{\T{metaid}^{\ssf{Type}}}}

  \RULE{\rt{type}}
  \CASE{\NT{ctype} \OR \mth{\T{metaid}^{\ssf{Type}}}}

  \RULE{\rt{pathToIsoFile}}
  \CASE{<.*>}
\end{grammar}

\include{examples}
\include{tips}
\end{document}

%%% Local Variables:
%%% mode: LaTeX
%%% TeX-master: "cocci_syntax"
%%% coding: latin-9
%%% TeX-PDF-mode: t
%%% ispell-local-dictionary: "american"
%%% End:
