aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Silence a warning that happens all too often in MacOS Xxleroy2011-05-121-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1654 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser: support for attributes over struct and union.xleroy2011-05-1217-135/+613
| | | | | | | | cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/StructAssign: always use __builtin_memcpy + alignment indicationxleroy2011-05-111-87/+53
| | | | | | | | | | (simpler and globally more efficient) cfrontend/C2C.ml: specialization of __builtin_memcpy over size */PrintAsm.ml: revised expansion of __builtin_memcpy_* ia32/Asm.ml: typo in comment git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-2/+0
| | | | | | | | | | Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 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
* Support compile-time constant expressions as arguments to gcc-style attributesxleroy2011-04-201-23/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1641 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use memcpy_word only if alignment AND size are multiples of word size.xleroy2011-04-171-3/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1638 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/Elab: __attribute, not attributexleroy2011-04-161-1/+1
| | | | | | | | ia32/PrintAsm: wrong section name regression: added test attribs1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1636 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of GCC attributes. Preliminary, untested support for ↵xleroy2011-04-143-17/+34
| | | | | | __aligned__ attribute git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1634 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of sizeof(string-literal)xleroy2011-03-151-5/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bitfields: MSB-to-LSB in addition to LSB-to-MSBxleroy2011-03-103-11/+39
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1600 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In StructAssign: be careful not to duplicate accesses to a volatile variable.xleroy2010-11-101-8/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1551 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Inconsistent treatment of "lone" zero-width bit fieldsxleroy2010-09-242-23/+31
| | | | | | | (i.e. not preceded by another bit field). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1516 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for IA32-Cygwin.xleroy2010-09-081-1/+1
| | | | | | | | cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adding __builtin_annotationxleroy2010-09-011-0/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of ↵xleroy2010-09-015-15/+68
| | | | | | reading a small unsigned bitfield git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1496 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-187-194/+440
| | | | | | | | | | | | | | | | | | | | | | - 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
* 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
* Preliminary support for gcc-style __attribute__ over typesxleroy2010-07-086-135/+168
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug in cparser/AddCasts.ml.xleroy2010-07-081-3/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1376 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* __builtin_memcpy, continued.xleroy2010-04-171-9/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1320 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-172-30/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1319 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.xleroy2010-04-098-54/+50
| | | | | | | | Algorithmic efficiency: in cparser/, precompute sizeof and alignof of composites. Code cleanup: introduced Cutil.composite_info_{def,decl} git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1312 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Static initialization of structs with bitfieldsxleroy2010-04-071-1/+74
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1311 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In cparser/SimplExpr.ml:xleroy2010-04-021-11/+15
| | | | | | | | - wrong simplification of && and || in the Set case - generated nicer code for && and || in the Eval case git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1308 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/AddCasts.ml: forgot to materialize cast at return statement.xleroy2010-04-011-12/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1307 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Handling of builtins, continued.xleroy2010-03-073-4/+9
| | | | | | | PrintCsyntax, PrintAsm: improve printing of float literals. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1284 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised treatment of builtinsxleroy2010-03-0710-244/+300
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for 'inline' modifierxleroy2010-03-034-20/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1272 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-0348-0/+9906
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 09:57:03 +0000