aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Ceval.ml
Commit message (Collapse)AuthorAgeFilesLines
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-5/+5
|
* Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-221-1/+1
| | | | | | | | | | | | | Several definitions in Cutil and elsewhere were accessing the default value of !Machine.config, before it is properly initialized in Driver. Delay evaluation of these definitions, and initialize Machine.config to nonsensical values so that lack of initialization is caught early (e.g. in Cutil.find_matching_*_kind). Also, following up on commit [3b8a094], don't use "wchar_t" typedef to type wide string literals, even if this typedef is in scope. The risk here is to hide an inconsistency between "wchar_t"'s definition in standard headers and CompCert's built-in definition.
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-211-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PackedStructs.ml: cleanups and bug-fixesxleroy2013-10-131-1/+1
| | | | | | | Ceval.ml: tolerate non-zero integers with pointer types. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2343 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove the C primitives for unsigned long long arithmetic, replacedxleroy2013-03-181-6/+25
| | | | | | | by pure OCaml code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2153 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppress int64_unsigned_to_float, now unused.xleroy2013-03-111-2/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2146 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+4
| | | | | | | cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-28/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-0/+5
| | | | | | | | | | and __alignof__(ty), __alignof__(expr) from GCC. - Resurrected __builtin_memcpy_aligned, useful for files generated by Scade KCG 6. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵xleroy2011-07-161-1/+3
| | | | | | | | | 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
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-081-0/+1
| | | | | | | | | | ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed. ia32/Asm.v: Pmov_ri can undef flags (if translated to xor) cparser/Ceval.ml: treat ~ in constant exprs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong cast in constant_exprxleroy2010-08-041-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-0/+277
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 08:26:51 +0000