aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Rename.ml
Commit message (Collapse)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+5
| | | | cfrontend/C2C.ml
* seems to process _Thread_local but not till backendDavid Monniaux2020-02-241-2/+5
|
* Remove the cparser/Builtins moduleXavier Leroy2019-07-171-1/+1
| | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
* Record value of constant expression in C.Scase constructorXavier Leroy2018-04-271-1/+1
| | | | | | | | | | | | The Elab pass checks that the argument of 'case' is a compile-time constant expression. This commit records the value of this expression in the C.Scase AST generated by Elab, so that it can be used for further diagnostics, i.e. checking (in Elab) for duplicate cases. Note that C2C ignores the recorded value and recomputes the value of the expression using Ceval.integer_expr. This is intentional: Ceval.integer_expr is more trustworthy, as it is formally verified against the CompCert C semantics.
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-1/+1
| | | | | | | | | | | | | | | | | | The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-1/+1
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Next try for support of anonymous structs.Bernhard Schommer2016-12-071-1/+2
| | | | | | Instead of using idents the anonymous fileds get names of the for <anon>_c where c is a counter of all anonymous members. Bug 20003
* Remove undocumented option. Bug 20193Bernhard Schommer2016-10-141-23/+6
|
* Classified all warnings and added various options.Bernhard Schommer2016-07-291-2/+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
* Handle large static initializers for global arraysXavier Leroy2015-11-091-1/+1
| | | | Use tail-recursive operations to implement transformations on initializers for global arrays. This way, very large static initializers no longer cause stack overflows at compile-time.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-8/+8
|
* Remove non digit and non letter chars from filename used in renaming of ↵Bernhard Schommer2015-07-151-0/+1
| | | | static variables to avoid problems with files such as "a b.c".
* Added flag for the renaming of static functions.Bernhard Schommer2015-05-191-6/+22
|
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-1/+7
|
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-211-10/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-0/+1
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).xleroy2012-12-181-4/+6
| | | | | | | 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
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-281-2/+2
| | | | | | | 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-9/+21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1831 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-0/+1
| | | | | | | | | | 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
* cparser: support for attributes over struct and union.xleroy2011-05-121-4/+5
| | | | | | | | 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
* Revised treatment of builtinsxleroy2010-03-071-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for 'inline' modifierxleroy2010-03-031-0/+1
| | | | 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-031-0/+253
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-05-19 17:02:10 +0000