aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/PrintCsyntax.ml
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-2/+2
|
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-4/+4
| | | | | | | | | | 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.
* In AST.calling_conventions, record whether the original C function was ↵Xavier Leroy2015-05-221-1/+1
| | | | | | "old-style" unprototyped. Use this info in printing function types for Csyntax and Clight.
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-2/+2
| | | | | | | | | | - 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
* Printing of EF_inline_asm builtins in GCC extended asm syntax.Xavier Leroy2015-04-211-0/+30
|
* Fix overflows in printers for clight and csyntax.Jacques-Henri Jourdan2015-04-011-1/+1
|
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-122/+19
|
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-131-2/+2
| | | | | | | | | | | The previous translation (in SimplExpr) produced references to the same temporary variable with two different types (bool and int), which is not nice if we want to typecheck the generated Clight. The new translation avoids this and also gets rid of the double cast to bool then to int. The trick is to change Eparen (in CompCert C expressions) to take two types: the type to which the argument must be converted, and the type with which the resulting expression is seen.
* Merge of "newspilling" branch:xleroy2014-07-231-0/+2
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Beautify the output.xleroy2014-02-211-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2414 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better printing of integer literals: add U and LL suffixes when needed.xleroy2014-01-121-9/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-26/+24
| | | | | | | | | | | | | | - 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 "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-11/+13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner printing of global variables.xleroy2013-11-091-21/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2364 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Recognize __builtin_fabs as an operator, not just a builtin,xleroy2013-11-061-0/+3
| | | | | | | | | enabling more aggressive optimizations. - Less aggressive CSE for EF_builtin builtins, causes problems for __builtin_write{16,32}_reversed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2363 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-051-1/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for debugging info (-g).xleroy2013-05-171-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+10
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-231-15/+13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-13/+14
| | | | | | | | | | | function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make Clight independent of CompCert C.xleroy2012-10-081-0/+2
| | | | | | | Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-1/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot to collect types of expressionsxleroy2012-07-281-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1984 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsxleroy2012-06-281-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better printing of pointer values and of locations.xleroy2012-02-291-10/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1830 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-1/+5
| | | | | | | | | | 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
* Don't print external declarations for builtins.xleroy2012-02-181-2/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1818 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:xleroy2012-02-041-23/+32
| | | | | | | | | | | | - 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
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-8/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-7/+10
| | | | | | | | test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-181-125/+131
| | | | | | | | | | | | | | | | | | | | | | - 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
* Updated Caml parts to match new representation for global variables.xleroy2010-05-261-10/+13
| | | | | | | */PrintAsm.ml: watch out for large stack frames in Pallocframe. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1349 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-1/+2
| | | | | | | Clight and C#minor. Recognize __builtin_fabs and turn it into this operator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Handling of builtins, continued.xleroy2010-03-071-29/+28
| | | | | | | PrintCsyntax, PrintAsm: improve printing of float literals. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1284 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Suppressed Init_pointer, now useless. Improved printing of strings in ↵xleroy2010-03-031-4/+0
| | | | | | generated .s git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1274 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-0/+6
| | | | | | | | | | | | Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive ↵xleroy2009-01-291-1/+0
| | | | | | file systems. Replaced CList by CoqList and likewise for CString and CInt. Removed useless references to CList in hand-written Caml code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+501
Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 01:28:13 +0000