blob: 344ab40e87a9d17c11492df7e985174bc35e574c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
\begin{figure}
\begin{syntax}
\syntaxclass{Types:}
{\it signedness} & ::= & "Signed" \alt "Unsigned" \\
{\it intsize} & ::= & "I8" \alt "I16" \alt "I32" \\
{\it floatsize} & ::= & "F32" \alt "F64" \\
\tau & ::= & "Tint" ({\it intsize}, {\it signedness}) \\
& \alt & "Tfloat" ({\it floatsize}) \\
& \alt & "Tvoid" \\
& \alt & "Tarray" (\tau, n) \\
& \alt & "Tpointer" (\tau) \\
% &\alt & "Tcomp_pointer" (\id) \\
&\alt & "Tstruct" (\id,\seq {(\id,\tau)}) \\
&\alt & "Tunion" (\id,\seq {(\id,\tau)}) \\
& \alt & "Tfunction" (\seq \tau, \tau)
%
\syntaxclass{Expressions annotated with types:}
a & ::= & \unannot{a}{\tau}
\syntaxclass{Unannotated expressions:}
b & ::= & \id & variable identifier\\
& \alt & n & integer constant\\
& \alt & f & float constant \\
& \alt & "sizeof"(\tau) & size of a type \\
& \alt & \op_1 ~ a & unary arithmetic operation\\
& \alt & a_1 ~\op_2 ~ a_2 & binary arithmetic operation\\
& \alt & \hbox{"*"} a & dereferencing \\
& \alt & a_1 [a_2] & array indexing \\
& \alt & a \dot \id & field access \\
& \alt & \hbox{"&"} a & address of \\
& \alt & (\tau) a & cast \\
& \alt & a_1 \hbox{" && "} a_2 \alt a_1 \hbox{" || "} a_2
& sequential boolean operations \\
& \alt & a(\seq a) & function call \\
%
\op_2 & ::= & \hbox{"+"} \alt \hbox{"-"} \alt \hbox{"*"} \alt \hbox{"/"} \alt \hbox{"%"}
& arithmetic operators \\
& \alt & \hbox{"<<"} \alt \hbox{">>"} \alt
\hbox{"&"} \alt \hbox{"|"} \alt \hbox{"^"}
& bitwise operators\\
& \alt & \hbox{"<"} \alt \hbox{"<="} \alt \hbox{">"} \alt \hbox{">="}
\alt \hbox{"=="} \alt \hbox{"!="}
& relational operators \\
\op_1 & ::= & \hbox{"-"} \alt \hbox{"~"} \alt \hbox{"!"}& unary operators
%
\end{syntax}
\caption{Abstract syntax of Clight (types and expressions). $\seq a$ denotes 0, 1 or several
occurrences of syntactic category $a$. $\opt a$ denotes an optional
occurrence of category $a$.}
\label{fig:syntax}
\end{figure}
|
