Changeset 207 for Deliverables/D3.1
 Timestamp:
 Oct 27, 2010, 4:27:28 PM (10 years ago)
 Location:
 Deliverables/D3.1/Report
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Report/report.tex
r197 r207 2 2 \usepackage[utf8x]{inputenc} 3 3 \usepackage{listings} 4 \usepackage{../ style/cerco}4 \usepackage{../../style/cerco} 5 5 \newcommand{\ocaml}{OCaml} 6 6 \newcommand{\clight}{Clight} 7 7 \newcommand{\matita}{matita} 8 \newcommand{\sdcc}{\texttt{sdcc}} 8 9 9 10 \newcommand{\textSigma}{\ensuremath{\Sigma}} … … 52 53 \vspace*{1cm} 53 54 \begin{center} 54 \includegraphics[width=0.6\textwidth]{../ style/cerco_logo.png}55 \includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png} 55 56 \end{center} 56 57 … … 80 81 \begin{large} 81 82 Main Authors:\\ 82 go here 83 Brian~Campbell, Randy~Pollack 83 84 \end{large} 84 85 \end{center} … … 103 104 elaborates C into an abstract syntax tree for the simpler \clight{} language, 104 105 based on the CIL C parser. The second part is a small step semantics for 105 \clight{} formalised by in the proof tool, which we have ported to \matita{}. 106 \clight{} formalised in the proof tool, which we have ported from Coq to the 107 \matita{} theorem prover. 106 108 This semantics is given in the form of inductive definitions, and so we have 107 109 added a third part giving an equivalent functional presentation in \matita{}. 108 110 109 The \cerco{} compiler alsoneeds to deal with the constrained memory model of111 The \cerco{} compiler needs to deal with the constrained memory model of 110 112 the target microcontroller (in our case, the 8051). Thus each part of the 111 113 semantics has been extended to allow explicit handling of the 112 microcontroller's memory spaces. 113 114 The port of the two stages of the CompCert \clight{} semantics is described in 115 Section~\ref{sec:port}. The new executable semantics is then discussed in 116 Section~\ref{sec:exec}, followed by the extensions for memory spaces in 117 Section~\ref{sec:memory}. Finally we discuss how the semantics can be tested 114 microcontroller's memory spaces. \emph{Cost labels} have also been added to 115 the \clight{} semantics to support the labelling approach to cost annotations 116 presented in~\cite{d2.1}. 117 118 The following section discusses the C language extensions for memory spaces. 119 Then the port of the two stages of the CompCert \clight{} semantics is 120 described in Section~\ref{sec:port}, followed by the new executable semantics 121 in Section~\ref{sec:exec}. Finally we discuss how the semantics can be tested 118 122 in Section~\ref{sec:valid}. 123 124 \section{Language extensions for the 8051 memory model} 125 \label{sec:ext} 126 127 The choice of an extended 8051 target for the \cerco{} compiler imposes an 128 irregular memory model with tight resource constraints. The different memory 129 spaces and access modes are summarised in Figure~\ref{fig:memorymodel}  130 essentially the development of the 8051 family has fragmented memory into 131 four regions: one half of the `internal' memory is fully accessible but also 132 contains the register banks, the second half cannot be directly addressed 133 because it is shadowed by the `Special Function Registers' (SFRs) for I/O; 134 `external memory' provides the bulk of memory in a separate address space; and 135 the code is in its own readonly space. 136 137 To make efficient use of the limited amount of memory, compilers for 8051 138 microcontrollers provide extra keywords to allocate global variables to 139 particular memory spaces, and to limit pointers to address a particular space. 140 The freely available \sdcc{} compiler provides the following extensions for 141 the 8051 memory spaces: 142 \begin{table}[ht] 143 \begin{tabular}{rcl} 144 Attribute & Pointer size & Memory space \\\hline 145 \lstinline'__data' & 1 & Internal, first half (0h  7fh) \\ 146 \lstinline'__idata' & 1 & Internal, indirect only (80h  ffh) \\ 147 \lstinline'__pdata' & 1 & External, page access (usually 0h  7fh) \\ 148 \lstinline'__xdata' & 2 & External, any (0h  ffffh) \\ 149 \lstinline'__code' & 2 & Code, any (0h  ffffh) \\ 150 \emph{none}& 3 & Any / Generic pointer 151 \end{tabular} 152 \end{table} 153 The generic pointers are a tagged union of the other kinds of pointers. 154 155 We intend the \cerco{} compiler to support extensions that are broadly 156 compatible with \sdcc{} to enable the compilation of programs with either. In 157 particular, this would allow the comparison of the behaviour of test cases 158 compiled with both compilers. Thus the C syntax and semantics have been 159 extended with the memory space attributes listed above. The syntax follows 160 \sdcc{} and in the semantics we track the memory space that each block was 161 allocated in and only permit access via the appropriate kinds of pointers. 162 The details on these changes are given in the following sections. 163 164 The \sdcc{} compiler also supports special variable types for accessing the 165 SFRs, which provide the standard I/O mechanism for the 8051 family. (Note 166 that pointers to these types are not allowed because only direct addressing of 167 the SFRs is allowed.) We intend to use CompCertstyle `external functions' 168 instead of special types. These are functions which are declared, but no C 169 implementation is provided. Instead they are provided by the runtime or 170 compiled directly to the corresponding machine code. This has the advantage 171 that no changes from the CompCert semantics are required, and a compatibility 172 library can be provided for \sdcc{} if necessary. The 8051 and the \sdcc{} 173 compiler also provide bitlevel access to a small region of internal memory. 174 We do not intend to expose this feature to C programs in the \cerco{} 175 compiler, and so no extension is provided for it. 119 176 120 177 \section{Port of CompCert \clight{} semantics to \matita{}} 121 178 \label{sec:port} 122 179 123 \begin{verbatim} 124 Smallstep inductive semantics. 125 Use CILbased parser from CompCert 1.7.1 (same as unverified prototype). 126 COST LABELS 127 \end{verbatim} 128 129 The first stage from the CompCert semantics is the parsing and elaboration of 130 C programs into the simpler \clight{} language. This is based upon the CIL 131 library for parsing, analysing and transforming C programs by Necula 132 et.~al.~\cite{cil02}. The elaboration performed provides explicit type 180 The first stage taken from the CompCert semantics is the parsing and 181 elaboration of C programs into the simpler \clight{} language. This is based 182 upon the CIL library for parsing, analysing and transforming C programs by 183 Necula et.~al.~\cite{cil02}. The elaboration performed provides explicit type 133 184 information throughout the program, including extra casts for promotion, and 134 185 performs simplifications such as breaking up expressions with side effects 135 into statements which perform the effects and effectfree expressions. The 136 resulting \clight{} programs are much more manageable and lack the ambiguities 137 of C, but remain easily understood by C programmers. 186 into statements that perform the effects using effectfree expressions. The 187 transformed \clight{} programs are much more manageable and lack the ambiguities 188 of C, but also remain easily understood by C programmers. 189 190 The parser has been extended with the 8051 memory spaces attributes given 191 above. The resulting abstract syntax tree records them on global variable 192 declarations and pointer types. However, we also need to deal with them 193 during the elaboration process to produce all of the required information. 194 For example, when the addressof operator \lstinline'&' is used it must decide 195 which kind of pointer should be used. Thus the extended elaboration process 196 keeps track of the memory space (if any) that the value of each 197 expression resides in. Where the memory space is not known, a generic pointer 198 will be used instead. Moreover, we also include the pointer kind when 199 determining whether a cast must be inserted so that conversions between 200 pointer representations can be performed. 201 202 203 Thus the elaboration turns the C code 204 \begin{quote} 205 \begin{lstlisting}[language=C] 206 int g(int *x) { return 5; } 207 208 int f(__data int *x, int *y) { 209 return x==y ? g(x) : *x; 210 } 211 212 __data int i = 1; 213 214 int main(void) { 215 return f(&i, &i); 216 } 217 \end{lstlisting} 218 \end{quote} 219 into the following Clight program: 220 \begin{quote} 221 \begin{lstlisting}[language=C] 222 int g(int *x) { return 5; } 223 224 int f(__data int * x, int * y) 225 { 226 int t; 227 if (x == (__data int * )y) { 228 t = g((int * )x); 229 } else { 230 t = *x; 231 } 232 return t; 233 } 234 235 int main(void) 236 { 237 int t; 238 t = f(&i, (int * )(&i)); 239 return t; 240 } 241 \end{lstlisting} 242 \end{quote} 243 The expressions in \lstinline'f' and \lstinline'main' had to be broken up due 244 to sideeffects, and casts have been added to change between generic pointers 245 and pointers specific to the \lstinline'__data' section of memory. The 246 underlying data structure also has types attached to every expression, but 247 these are inconvenient to show in source form. 138 248 139 249 Note that the translation from C to \clight{} is not proven correct  … … 141 251 can have some confidence in the code, however, because it has received testing 142 252 in the \cerco{} prototype, and it is very close to the version used in 143 CompCert. As we also have an executable semantics we can perform testing of 144 it without involving the rest of the compiler. Moreover, the careful 145 programmer could choose to inspect the \clight{} code, or even work entirely 146 in the \clight{} language. 147 \todo{cite compcert discussion on CIL} 148 \todo{some details on what CIL does and example before/after} 253 CompCert. We can also perform testing of the semantics without involving the 254 rest of the compiler because we have an executable semantics. Moreover, the 255 cautious programmer could choose to inspect the \clight{} code, or even work 256 entirely in the \clight{} language. 149 257 150 258 The semantics for \clight{} itself has been ported from the Coq development 151 used in CompCert to \matita{} for use in CerCo. Details about the original259 used in CompCert to \matita{} for use in \cerco{}. Details about the original 152 260 bigstep formalisation of \clight{} can be found in Leroy and 153 Blazy~\cite{compcertmm08}, although we started from a later version with a 261 Blazy~\cite{compcertmm08} (including a discussion of the translation from C 262 in \S 4.1), although we started from a later version with a 154 263 smallstep semantics and hence support for \lstinline'goto' statements. 155 264 Several parts of the semantics were shared with other parts of the CompCert … … 160 269 \item traces of I/O events, 161 270 \item a memory model that keeps conceptually distinct sections of memory 162 separate (assigning `undefined behaviour' to a buffer overflow, for instance), 163 \item resulting about composing execution steps of arbitrary smallstep 271 strictly separate (assigning `undefined behaviour' to a buffer overflow, for 272 instance), 273 \item results about composing execution steps of arbitrary smallstep 164 274 semantics, 165 275 \item data structures for local and global environments, and … … 167 277 \end{itemize} 168 278 We anticipate a similar arrangement for the \cerco{} verified compiler, 169 although this means that there may be further changes to the separts of the279 although this means that there may be further changes to the common parts of the 170 280 semantics later in the project to harmonise the stages of the compiler. 171 281 … … 184 294 \begin{quote} 185 295 \begin{lstlisting} 186 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace →Prop ≝187 ... 188  eval_Elvalue: ∀a,ty,psp,loc,ofs,v,tr.189 eval_lvalue ge e m (Expr a ty) psp loc ofs tr →190 load_value_of_type ty m psp loc ofs = Some ? v →296 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr $\rightarrow$ val $\rightarrow$ trace $\rightarrow$ Prop ≝ 297 ... 298  eval_Elvalue: $\forall$a,ty,psp,loc,ofs,v,tr. 299 eval_lvalue ge e m (Expr a ty) psp loc ofs tr $\rightarrow$ 300 load_value_of_type ty m psp loc ofs = Some ? v $\rightarrow$ 191 301 eval_expr ge e m (Expr a ty) v tr 192 302 \end{lstlisting} … … 196 306 and offset into the block, respectively. The expression can thus evaluate to 197 307 the value \lstinline'v' if \lstinline'v' can be loaded from that location. 198 One corresponding part of the \lstinline'eval_lvalue' definition, 199 \begin{quote} 200 \begin{lstlisting} 201 ... 202 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝ 203  eval_Evar_local: ∀id,l,ty. 204 get ??? id e = Some ? l → 308 One corresponding part of the \lstinline'eval_lvalue' definition is 309 \begin{quote} 310 \begin{lstlisting} 311 ... 312 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : 313 expr $\rightarrow$ memory_space $\rightarrow$ block $\rightarrow$ int $\rightarrow$ trace $\rightarrow$ Prop ≝ 314  eval_Evar_local: $\forall$id,l,ty. 315 get ??? id e = Some ? l $\rightarrow$ 205 316 eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0 206 317 ... … … 219 330 The only new expression in our semantics is the cost label which wraps around 220 331 another expression. It does not change the result, but merely adds the given 221 label to the trace so as to identify the branches taken in conditional 222 expressions so that accurate cost information can be attached to the program. 332 label to the trace to identify the branches taken in conditional 333 expressions so that accurate cost information can be attached to the program: 334 \begin{quote} 335 \begin{lstlisting} 336  eval_Ecost: $\forall$a,ty,v,l,tr. 337 eval_expr ge e m a v tr $\rightarrow$ 338 eval_expr ge e m (Expr (Ecost l a) ty) v (tr++Echarge l) 339 \end{lstlisting} 340 \end{quote} 223 341 \todo{make the semantics of the cost labels clearer} 224 342 … … 230 348 ninductive state: Type := 231 349  State: 232 ∀f: function.233 ∀s: statement.234 ∀k: cont.235 ∀e: env.236 ∀m: mem. state350 $\forall$f: function. 351 $\forall$s: statement. 352 $\forall$k: cont. 353 $\forall$e: env. 354 $\forall$m: mem. state 237 355  Callstate: 238 ∀fd: fundef.239 ∀args: list val.240 ∀k: cont.241 ∀m: mem. state356 $\forall$fd: fundef. 357 $\forall$args: list val. 358 $\forall$k: cont. 359 $\forall$m: mem. state 242 360  Returnstate: 243 ∀res: val.244 ∀k: cont.245 ∀m: mem. state.361 $\forall$res: val. 362 $\forall$k: cont. 363 $\forall$m: mem. state. 246 364 \end{lstlisting} 247 365 \end{quote} … … 262 380 \begin{quote} 263 381 \begin{lstlisting} 264 ninductive step (ge:genv) : state → trace → state →Prop ≝265  step_assign: ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.266 eval_lvalue ge e m a1 psp loc ofs tr1 →267 eval_expr ge e m a2 v2 tr2 →268 store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' →382 ninductive step (ge:genv) : state $\rightarrow$ trace $\rightarrow$ state $\rightarrow$ Prop ≝ 383  step_assign: $\forall$f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2. 384 eval_lvalue ge e m a1 psp loc ofs tr1 $\rightarrow$ 385 eval_expr ge e m a2 v2 tr2 $\rightarrow$ 386 store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' $\rightarrow$ 269 387 step ge (State f (Sassign a1 a2) k e m) 270 (tr1 ⧺tr2) (State f Sskip k e m')271 ... 272 \end{lstlisting} 273 \end{quote} 274 which can be read as , if388 (tr1++tr2) (State f Sskip k e m') 389 ... 390 \end{lstlisting} 391 \end{quote} 392 which can be read as: 275 393 \begin{itemize} 276 \item \lstinline'a1' can evaluate to the location \lstinline'psp,loc,ofs',394 \item if \lstinline'a1' can evaluate to the location \lstinline'psp,loc,ofs', 277 395 \item \lstinline'a2' evaluates to a value \lstinline'v2', and 278 396 \item storing \lstinline'v2' at location \lstinline'psp,loc,ofs' succeeds, … … 294 412 \begin{quote} 295 413 \begin{lstlisting} 296  step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.297 event_match (external_function id targs tres) vargs t vres →414  step_external_function: $\forall$id,targs,tres,vargs,k,m,vres,t. 415 event_match (external_function id targs tres) vargs t vres $\rightarrow$ 298 416 step ge (Callstate (External id targs tres) vargs k m) 299 417 t (Returnstate vres k m) … … 321 439 \begin{quote} 322 440 \begin{lstlisting} 323 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val×trace. eval_expr ge en m e (\fst r) (\snd r)) ≝ 441 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : 442 res ($\Sigma$r:val$\times$trace. eval_expr ge en m e (\fst r) (\snd r)) ≝ 324 443 match e with 325 [ Expr e' ty ⇒444 [ Expr e' ty $\Rightarrow$ 326 445 match e' with 327 446 [ ... 328  Evar _ ⇒Some ? (329 do 〈l,tr〉 ←exec_lvalue' ge en m e' ty;330 do v ←opt_to_res ? (load_value_of_type' ty m l);331 OK ? 〈v,tr〉)447  Evar _ $\Rightarrow$ Some ? ( 448 do $\langle$l,tr$\rangle$ $\leftarrow$ exec_lvalue' ge en m e' ty; 449 do v $\leftarrow$ opt_to_res ? (load_value_of_type' ty m l); 450 OK ? $\langle$v,tr$\rangle$) 332 451 ... 333 452 ] 334 453 ] 335 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝ 454 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : 455 res ($\Sigma$r:memory_space $\times$ block $\times$ int $\times$ trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝ 336 456 match e' with 337 [ Evar id ⇒457 [ Evar id $\Rightarrow$ 338 458 match (get … id en) with 339 [ None ⇒ Some ? (do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)340  Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *)459 [ None $\Rightarrow$ Some ? (do $\langle$sp,l$\rangle$ $\leftarrow$ opt_to_res ? (find_symbol ? ? ge id); OK ? $\langle$$\langle$$\langle$sp,l$\rangle$,zero$\rangle$,E0$\rangle$) (* global *) 460  Some loc $\Rightarrow$ Some ? (OK ? $\langle$$\langle$$\langle$Any,loc$\rangle$,zero$\rangle$,E0$\rangle$) (* local *) 341 461 ] 342 462 ... … … 349 469 \begin{quote} 350 470 \begin{lstlisting} 351 do x ←e; e'471 do x $\leftarrow$ e; e' 352 472 \end{lstlisting} 353 473 \end{quote} … … 360 480 coercion between the types 361 481 \begin{center} 362 \lstinline'option res T' \quad and \quad \lstinline'res (Σx:T. P x)'482 \lstinline'option (res T)' \quad and \quad \lstinline'res ($\Sigma$x:T. P x)' 363 483 \end{center} 364 484 (where a branch marked \lstinline'None' would generate a proof obligation to … … 376 496 `external' functions for I/O, which can return arbitrary values. These are 377 497 handled by a resumption monad, which on encountering some I/O returns a 378 suspension that when applied to a value resumes the evaluation of the 379 semantics. Resumption monads are a standard tool for providing denotational 380 semantics for input~\cite{Moggi199155} and interleaved concurrency~\cite{??}. 498 suspension. When the suspension is applied to a value the evaluation of the 499 semantics is resumed. Resumption monads are a standard tool for providing 500 denotational semantics for input~\cite{Moggi199155} and interleaved 501 concurrency~\cite{??}. 381 502 The definition also incorporates errors, and uses a coercion to automatically 382 503 transform values from the plain error monad. … … 386 507 \begin{quote} 387 508 \begin{lstlisting} 388 nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out ( Σr:trace ×state. step ge st (\fst r) (\snd r))) ≝509 nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out ($\Sigma$r:trace $\times$ state. step ge st (\fst r) (\snd r))) ≝ 389 510 match st with 390 [ State f s k e m ⇒511 [ State f s k e m $\Rightarrow$ 391 512 match s with 392 [ Sassign a1 a2 ⇒Some ? (393 ! 〈l,tr1〉 ←exec_lvalue ge e m a1;:394 ! 〈v2,tr2〉 ←exec_expr ge e m a2;:395 ! m' ←store_value_of_type' (typeof a1) m l v2;:396 ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)513 [ Sassign a1 a2 $\Rightarrow$ Some ? ( 514 ! $\langle$l,tr1$\rangle$ $\leftarrow$ exec_lvalue ge e m a1;: 515 ! $\langle$v2,tr2$\rangle$ $\leftarrow$ exec_expr ge e m a2;: 516 ! m' $\leftarrow$ store_value_of_type' (typeof a1) m l v2;: 517 ret ? $\langle$tr1++tr2, State f Sskip k e m'$\rangle$) 397 518 ... 398 519 \end{lstlisting} … … 405 526 \begin{quote} 406 527 \begin{lstlisting} 407 do_io : ident → list eventval →IO eventval io_out eventval528 do_io : ident $\rightarrow$ list eventval $\rightarrow$ IO eventval io_out eventval 408 529 \end{lstlisting} 409 530 \end{quote} … … 413 534 ... 414 535 ] 415  Callstate f0 vargs k m ⇒536  Callstate f0 vargs k m $\Rightarrow$ 416 537 match f0 with 417 538 [ ... 418  External f argtys retty ⇒Some ? (419 ! evargs ←check_eventval_list vargs (typlist_of_typelist argtys);:420 ! evres ←do_io f evargs;:421 ! vres ←check_eventval evres (proj_sig_res (signature_of_type argtys rett422 ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)539  External f argtys retty $\Rightarrow$ Some ? ( 540 ! evargs $\leftarrow$ check_eventval_list vargs (typlist_of_typelist argtys);: 541 ! evres $\leftarrow$ do_io f evargs;: 542 ! vres $\leftarrow$ check_eventval evres (proj_sig_res (signature_of_type argtys rett 543 ret ? $\langle$(Eextcall f evargs evres), Returnstate vres k m$\rangle$) 423 544 ... 424 545 \end{lstlisting} … … 426 547 \todo{say something more about the rest?} 427 548 428 \todo{``the valid''?} 429 Together with functions to provide a valid initial state for a program and to 549 Together with functions to provide the initial state for a program and to 430 550 detect a final state we can write a function to run the program up to a given 431 551 number of steps. Similarly, a corecursive function can return the entire … … 433 553 434 554 \todo{completeness?} 435 436 \begin{verbatim}437 Functional version of the semantics.438 Soundness given in dependent type of execution functions, using Russellstyle439 separation of terms and proofs. Pattern matching mimicks inductive definitions from smallstep semantics. Error monad to deal with undefined behaviour;440 IO monad with handling of I/O by resumption (which incorporates errors too).441 \end{verbatim}442 443 \section{8051 memory spaces}444 \label{sec:memory}445 446 \begin{verbatim}447 Share quite a bit with the 8051 doc.448 449 Outline of 8051 memory.450 451 Semantic changes: Values: Blocks in the memory model carry space they are in452 (or \texttt{Any} if unspecified; pointers carry space they can point at (or453 \texttt{Any} for a generic pointer which can refer to any block). Types:454 pointers carry space corresponding to the allowed pointer values (arrays similar455 because they degrade into pointers). (Not456 redundant: pointers can be put into a sufficiently large integer then recast to457 their original type. Cast must be undefined if spaces don't match.) Operations: casts, comparisons, addition and subtraction.458 459 Syntactic changes: Clight, pointer and array types, and global decls have spaces added. CIL similarly changed, but had to tracking space for expr in the elaboration to discover spaces for types.460 \end{verbatim}461 555 462 556 \section{Validation}
Note: See TracChangeset
for help on using the changeset viewer.