aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Collapse)AuthorAgeFilesLines
* Improved error messages for wrong vararg calls.Bernhard Schommer2016-09-231-2/+7
| | | | | | Now "expected at least %d" instead of "expected %d". Also improved error message for __builtin_debug. Bug 19872
* Catch case of zero in builtin debug.Bernhard Schommer2016-09-221-2/+2
|
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-211-5/+8
|\ | | | | | | | | | | Fix minor issues in some proofs and tactics. Patch by Maxime Dénès.
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-211-5/+8
| | | | | | | | | | These minor problems were revealed by porting CompCert to Coq 8.6, where they trigger errors.
* | Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-202-36/+34
|\ \ | | | | | | Advanced diagnostics
| * | Readded warning about ignored volatile. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Added missing literal. Bug 18004Bernhard Schommer2016-08-311-1/+1
| | |
| * | Fixed typos.Bernhard Schommer2016-08-311-8/+8
| | | | | | | | | | | | | | | | | | Removed duplicated of, changed string to string literal for wording than the C standard. Bug 18004
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-1/+1
| | |
| * | Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-292-3/+23
| |\ \
| * | | Classified all warnings and added various options.Bernhard Schommer2016-07-292-34/+33
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | 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
* | | Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-31/+4
| | | | | | | | | | | | Inline directives in extraction.v make the Caml output efficient and almost nice.
* | | Removed some implict arguments.Bernhard Schommer2016-09-051-13/+5
| |/ |/| | | | | Also changed Local Open to Open Local.
* | Simplify test. Bug 19629Bernhard Schommer2016-08-251-4/+1
| |
* | Test for illegal first argument in __builtin_debug.Bernhard Schommer2016-08-251-2/+6
| | | | | | | | | | | | | | The test is extended for integer constants smaller than 0. Also the default constant used for the error is no longer 0 since this is not a positive number. Bug 19629
* | Print prototypes for malloc and free.Bernhard Schommer2016-08-231-1/+1
| | | | | | | | | | | | The declarations of malloc and free should also be printed for CompCert C. Bug 19616.
* | Also print declarations in CompCert C.Bernhard Schommer2016-08-221-0/+20
| | | | | | | | | | | | The PrintCsyntax now first emits declarations for all functions and variables in order to allow foward declarations. Bug 19598.
* | Added missing , in PrintCsyntax. Bug 19599Bernhard Schommer2016-08-221-1/+1
|/
* Port to Coq 8.5pl2Xavier Leroy2016-07-082-2/+1
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-1/+1
| | | | | | | | Most of the code can be String.uppercase usages can either be replaced by a more specialized version of coqstring_of_camlstring (which is also slightly more effecient) or by specialized checks that reject wrong code earlier. Bug 19187
* fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert ↵Michael Schmidt2016-06-071-1/+1
| | | | can parse its own .compcert.c output, bug 18060
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-172-3/+3
| | | | | | | | | | | | | This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations. In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves. Summary of changes: - AST: introduce the type "rpair A" of register pairs - Conventions1, Conventions: use it when describing calling conventions - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls - Events: suppress external_call', no longer useful - All passes from Allocation to Asmgen: adapt accordingly.
* Merge branch 'master' into cleanupBernhard Schommer2016-03-2123-989/+1493
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-2018-649/+1093
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This pull request implements "approach A" to separate compilation in CompCert from the paper Lightweight verification of separate compilation by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis, POPL 2016, pages 178-190 In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program. This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
| | * Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-0611-533/+559
| | |
| | * Define linking for Csyntax and Clight programs.Xavier Leroy2016-03-063-114/+523
| | | | | | | | | | | | Also: factor out the type "program" between Csyntax and Clight, putting it in Ctypes.
| | * Add support for EF_runtime externalsXavier Leroy2016-03-064-2/+11
| | | | | | | | | | | | Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-152-6/+6
| | | | | | | | | | | | | | | | | | As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always). Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing.
| * | Merge pull request #90 from AbsInt/sem-castsXavier Leroy2016-03-1114-323/+368
| |\ \ | | | | | | | | Make casts of pointers to _Bool semantically well defined
| | * | Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-0214-323/+368
| | |/ | | | | | | | | | | | | | | | In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds). Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL. Hence, this kind of casts was temporarily given undefined semantics. This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid. This reinstates the equivalence between casts to _Bool and comparisons != 0. The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass. The pass was lightly modified to work around the issue.
| * / Relaxing the semantics of pointer arithmetic.Xavier Leroy2016-02-291-6/+21
| |/ | | | | | | | | | | Support <pointer> +/- <integer> where the pointer value is actually an integer (Vint) that has been converted to pointer type. Such arithmetic, while not defined in ISO C, appears in the wild. If present in static initializers, it used to cause a compile-time failure ("not a compile-time constant"). Hence this relaxation.
* | Removed not needed env.Bernhard Schommer2016-03-151-5/+5
| | | | | | | | | | | | The functions for naming string and wstring literals no longer need an env. Bug 18394
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-153-38/+38
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-151-3/+3
| | | | | | | | This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
* | Removed unused parameter from is_small/rel_data.Bernhard Schommer2016-03-111-3/+3
| | | | | | | | | | | | The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394
* | Code cleanup.Bernhard Schommer2016-03-103-102/+93
|/ | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* Restart the name generator at first_unused_ident for every function.Xavier Leroy2016-02-053-58/+38
| | | | This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.
* Revise and simplify the -fstruct-return and -fstruct-passing options.Xavier Leroy2015-12-081-11/+18
| | | | | | - Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing' - Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful. - Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code.
* Handle large static initializers for global arraysXavier Leroy2015-11-093-118/+205
| | | | 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.
* Fix for switch was to eager.Bernhard Schommer2015-11-061-6/+8
| | | | | | We should not remove any debug stmt inside of the cases. We should just not warn in the case that init is only debugcalls. Bug 17850
* Remove debug stmts during grouping of switch.Bernhard Schommer2015-11-061-3/+5
| | | | | | | Debug statements introduced during the translation result in warnings when they are introduced at the head of the switch. Since they are not used and the warning is not necessary we can remove them before. Fix 17580.
* Added printing functions for debug annotations.Bernhard Schommer2015-11-061-0/+3
| | | | | | Instead of printing <unknown builtin> we now print the debug annotations. Fix 17581.
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-201-2/+2
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/TargetPrinter.ml backend/CMparser.mly backend/SelectLongproof.v backend/Selectionproof.v cfrontend/C2C.ml checklink/Asm_printers.ml checklink/Check.ml checklink/Fuzz.ml common/AST.v debug/DebugInformation.ml debug/DebugInit.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli debug/Dwarfgen.ml exportclight/ExportClight.ml ia32/TargetPrinter.ml powerpc/Asm.v powerpc/SelectOpproof.v powerpc/TargetPrinter.ml
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1420-1989/+1989
| |
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-41/+41
| |
| * Unified function for adding the atom identifier.Bernhard Schommer2015-10-121-2/+2
| | | | | | | | | | | | | | Instead of defining two functions for adding the mapping from atom to debug id we use one function which then sets the corresponding values. Bug 17392.
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2023-2030/+2030
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-113-14/+15
|/ | | | | | | | | | The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
* Fixed minor issue with parameters that get put on the stack, madeBernhard Schommer2015-09-301-4/+6
| | | | the code more robust and added indentation for convertCompositeDef
* Added location for the formal parameters and move the end of allBernhard Schommer2015-09-281-0/+1
| | | | scopes before the last statement.
generated by cgit (git 2.34.1) at 2024-07-01 15:49:28 +0000