-
- Downloads
Merge of branches/full-expr-4:
- Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 12 additions, 8 deletions.depend
- Makefile 4 additions, 2 deletionsMakefile
- arm/Op.v 1 addition, 1 deletionarm/Op.v
- arm/PrintOp.ml 115 additions, 0 deletionsarm/PrintOp.ml
- backend/CastOptim.v 276 additions, 0 deletionsbackend/CastOptim.v
- backend/CastOptimproof.v 577 additions, 0 deletionsbackend/CastOptimproof.v
- backend/Coloringaux.ml 18 additions, 9 deletionsbackend/Coloringaux.ml
- backend/PrintCminor.ml 285 additions, 0 deletionsbackend/PrintCminor.ml
- backend/PrintLTLin.ml 130 additions, 0 deletionsbackend/PrintLTLin.ml
- backend/PrintRTL.ml 50 additions, 9 deletionsbackend/PrintRTL.ml
- backend/RTLgen.v 17 additions, 23 deletionsbackend/RTLgen.v
- backend/RTLgenproof.v 13 additions, 61 deletionsbackend/RTLgenproof.v
- backend/RTLgenspec.v 38 additions, 66 deletionsbackend/RTLgenspec.v
- cfrontend/C2Clight.ml 171 additions, 150 deletionscfrontend/C2Clight.ml
- cfrontend/Clight.v 623 additions, 0 deletionscfrontend/Clight.v
- cfrontend/Cminorgen.v 38 additions, 228 deletionscfrontend/Cminorgen.v
- cfrontend/Cminorgenproof.v 442 additions, 679 deletionscfrontend/Cminorgenproof.v
- cfrontend/Csem.v 617 additions, 1176 deletionscfrontend/Csem.v
- cfrontend/Csharpminor.v 104 additions, 87 deletionscfrontend/Csharpminor.v
- cfrontend/Cshmgen.v 134 additions, 162 deletionscfrontend/Cshmgen.v
Loading
Please register or sign in to comment