Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵ | xleroy | 2011-07-16 | 1 | -122/+119 |
| | | | | | | | | | the type of the whole conditional expression. Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Merge of branch new-semantics: revised and strengthened top-level statements ↵ | xleroy | 2011-07-15 | 1 | -7/+4 |
| | | | | | | of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Removed useless constraints on return type at Sreturn instructions | xleroy | 2010-08-18 | 1 | -3/+2 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Merge of branches/full-expr-4: | xleroy | 2010-08-18 | 1 | -0/+1851 |
- 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 |