aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
Commit message (Collapse)AuthorAgeFilesLines
...
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-1/+1
|\
| * 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
* | Classified all warnings and added various options.Bernhard Schommer2016-07-291-33/+32
|/ | | | | | | | | | 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
* 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
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-2/+4
|\
| * Add support for EF_runtime externalsXavier Leroy2016-03-061-0/+2
| | | | | | | | Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
* | 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-151-27/+27
| | | | | | | | | | | | 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-101-73/+71
|/ | | | | | 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.
* 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-091-5/+5
| | | | 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.
* 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-141-38/+38
| |
| * 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-201-38/+38
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-6/+7
|/ | | | | | | | | | 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.
* Merge branch 'debugscopes' into debug_locationsBernhard Schommer2015-09-211-38/+36
|\ | | | | | | | | | | Conflicts: debug/CtoDwarf.ml debug/DwarfPrinter.ml
| * Experiment: track the scopes of local variables via __builtin_debug.Xavier Leroy2015-09-201-38/+36
| | | | | | | | | | | | | | | | | | | | | | C2C: the code that insert debug builtins with the line numbers is now in Unblock. Handle calls to __builtin_debug. Unblock: generate __builtin_debug(1) for line numbers, carrying the list of active scopes as extra arguments. Generate __builtin_debug(6) for local variable declarations, carrying the corresponding scope number as extra argument. Constprop: avoid duplicating debug arguments that are constants already. PrintAsmaux: show this extra debug info as comments.
* | Started implementing the scope for the Debug Informations.Bernhard Schommer2015-09-181-0/+1
| | | | | | | | | | | | Scopes will be handled by a stack of all open scopes. This stack then can also be used to generate the debug directives to track the scopes through the rest of the passes.
* | First version with computation of dwarf info from debug info.Bernhard Schommer2015-09-171-1/+1
| | | | | | | | | | Introduced a new dwarf generation from the information collected in the DebugInformation and removed the old CtODwarf translation.
* | Move more functionality in the new interface.Bernhard Schommer2015-09-161-4/+7
| | | | | | | | | | | | 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.
* | XBernhard Schommer2015-09-061-1/+1
|\| | | | | | | Merge branch 'master' into debug_locations
| * Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-1/+1
| | | | | | | | | | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
* | Added symbol functions for printing of the location for global variables.Bernhard Schommer2015-08-211-2/+8
|/
* Tighten and prove correct the underflow/overflow bounds for parsing of FP ↵Xavier Leroy2015-07-061-41/+29
| | | | | | | | | literals. This is a follow-up to commit 350354c. - Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse - Add early checks for overflow and underflow and prove them correct. - Improve speed of Bparse by using a fast exponentiation (square-and-multiply).
* Added a fast test for too large exponents too avoid never ending computations.Bernhard Schommer2015-07-031-29/+42
|
* Check also the discarded part of the switch statements for cases outside of ↵Bernhard Schommer2015-06-261-1/+26
| | | | an switch to bail out on earlier on unstructured switch.
* In AST.calling_conventions, record whether the original C function was ↵Xavier Leroy2015-05-221-9/+11
| | | | | | "old-style" unprototyped. Use this info in printing function types for Csyntax and Clight.
* Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-211-4/+2
| | | | | | | | | | | | Ctyping: define a typechecker for whole programs. Csyntax: introduce the type "pre-program" (non-dependent). C2C: use Ctyping.econdition instead of Ctyping.econdition'. Note: Ctyping.typecheck_program could be used as the first step in the verified compilation pipeline. Then, retyping would no longer be performed in C2C. We keep it this way (for the time being) because retyping errors are reported more precisely in C2C than in Ctyping.
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-1/+1
| | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* Warn if a nonzero FP literal converts to infinity (overflow) or to 0 ↵Xavier Leroy2015-04-251-3/+17
| | | | | | (underflow). Also: spurious '\n' in C2C.warning.
* Use Cerrors for error reporting instead of rolling our own reporting in C2C.Xavier Leroy2015-04-211-11/+5
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-211-80/+15
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-2/+93
|
* Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-011-2/+1
|\ | | | | Extended annotations
| * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-2/+1
| |
* | Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-201-13/+37
|/ | | | ARM is done, IA32 and PowerPC remain to be updated.
* Issue #28: if the arguments of __builtin_memcpy_aligned are arrays, their ↵Xavier Leroy2015-03-101-1/+3
| | | | types must decay to pointer types in the "types" part of Ebuiltin.
* Merge branch 'named-structs'Xavier Leroy2015-01-231-212/+183
|\ | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
| * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-64/+80
| | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
| * Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-148/+103
| |
* | Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-221-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-201-1/+54
| | | | | | | | | | | | | | | | | | | | This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions.
generated by cgit (git 2.34.1) at 2024-07-02 09:16:23 +0000