aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Parse.ml
Commit message (Collapse)AuthorAgeFilesLines
* Remove undocumented option. Bug 20193Bernhard Schommer2016-10-141-1/+1
|
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-0/+1
|\
| * Added error check before transformations.Bernhard Schommer2016-08-081-0/+1
| | | | | | | | | | | | Added a check for errors after the elab phases to avoid problems in the transformations due to broken input programs. Bug 19504
* | Classified all warnings and added various options.Bernhard Schommer2016-07-291-1/+1
|/ | | | | | | | | | Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
* Open files in binary mode.Bernhard Schommer2015-11-301-1/+1
| | | | | | On windows opening files in text mode can result in errors due to non-windows compatible input. Thus open files only in binary mode. Bug 17664
* Read the whole source C file into memory instad of reading it on demand.François Pottier2015-10-231-3/+15
| | | | | Having the file in memory will help build an error message. Also, this may be slightly faster.
* Merge pull request #57 from jhjourdan/parser_fixBernhard Schommer2015-10-011-3/+7
|\ | | | | Correction of a few bugs in the pre-parser, added comments.
| * Fixed a few bugs in the pre parser. In particular, the following codeJacques-Henri Jourdan2015-09-301-3/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | was not parsed correctly: typedef int a; int f() { for(int a; ;) if(1); a * x; } Additionnaly, I tried to add some comments in the pre-parser code, especially for the different hacks used to solve various conflicts.
* | Move more functionality in the new interface.Bernhard Schommer2015-09-161-9/+4
|/ | | | | | Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom.
* Added flag for the renaming of static functions.Bernhard Schommer2015-05-191-1/+1
|
* Bitfield improvements continued: perform bitfield expansion before ↵Xavier Leroy2015-04-281-1/+1
| | | | unblocking; improve translation of bitfield initializers and compound literals.
* Compute the size of structs using the result of the packing and bitfield ↵Bernhard Schommer2015-03-261-10/+10
| | | | transformations.
* Added missing functions for printing the structs and unions. Still missing ↵Bernhard Schommer2015-03-241-4/+9
| | | | printing of packed structs.
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-291-3/+3
|
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-4/+12
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-061-6/+10
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-281-4/+4
| | | | | | | cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problems with multiple declarations of publically-visible identifiersxleroy2012-02-291-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1831 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:xleroy2012-02-041-12/+2
| | | | | | | | | | | | - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* SimplVolatile: new pass to eliminate read-modify-write ops over volatilesxleroy2011-08-181-3/+5
| | | | | | | | Elsewhere: refactoring, moving common code into Cutil and Transform (to be continued) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1716 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser: support for attributes over struct and union.xleroy2011-05-121-1/+3
| | | | | | | | 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
* Merge of branches/full-expr-4:xleroy2010-08-181-3/+3
| | | | | | | | | | | | | | | | | | | | | | - 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
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-0/+59
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e