aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/PrintClight.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
* Oexpect in frontendDavid Monniaux2020-04-071-0/+1
|
* -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| | | | | | | | | | | | | | | | | | | | | The temporary variables introduced by SimplLocals reuse the same integer identifiers as the local variables they come from. This commit ensures that these variables are printed as "$var", where "var" is the original variable name, instead of "$NNN" as before. The "$NNN" form is retained for temporary variables that do not correspond to a source-level local variable, such as the temporary variables introduced by SimplExpr. This commit should make no difference for "ccomp -dclight", because the Clight that is printed is the Clight version 1 produced by SimplExpr, where every temporary is fresh and does not correspond to a source-level local variable. This commit does change the output of "clightgen -dclight", because the Clight that is printed is the Clight version 2 produced by SimplLocals. The printed Clight is much more legible thanks to the more meaningful temporary variable names.
* clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-161-11/+30
| | | | | | | | | | | | | The Clight output of clightgen is Clight version 2, after SimplLocals conversion, where function parameters are temporary variables, not variables. This commit makes sure the function parameters are printed as temporary variables and not as variables. In passing, it generalizes the Clight pretty-printer so that it can print both Clight version 1 and Clight version 2. Closes: #314
* Pull request #192: improve the printing of Clight intermediate codeXavier Leroy2017-11-221-10/+26
| | | | So that it looks more like valid C source.
* Inlined open of ASTBernhard Schommer2017-02-061-7/+6
|
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-1/+1
| | | | | | | | | | | | | 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-211-4/+4
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-201-1/+1
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Add support for EF_runtime externalsXavier Leroy2016-03-061-1/+1
| | | | | | | | | | | | 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-151-2/+2
| |/ | | | | | | | | | | 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.
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-4/+4
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Code cleanup.Bernhard Schommer2016-03-101-13/+9
|/ | | | | | 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.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-1/+1
|
* 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-63/+8
|
* Merge of "newspilling" branch:xleroy2014-07-231-0/+4
| | | | | | | | | | | | | | | - 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
* Better printing of integer literals: add U and LL suffixes when needed.xleroy2014-01-121-0/+4
| | | | 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-5/+5
| | | | | | | | | | | | | | - 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
* - Recognize __builtin_fabs as an operator, not just a builtin,xleroy2013-11-061-0/+2
| | | | | | | | | 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
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+4
| | | | | | | | | 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-28/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Camlcoq.ml: bug in conversion Z to stringv1.12.1xleroy2013-01-291-1/+1
| | | | | | | PrintClight: forgot "$" prefix on temporary names git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2102 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-2/+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-12/+13
| | | | | | | | | | | 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-1/+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-25/+28
| | | | 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-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-4/+0
| | | | | | | | | | 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-19/+3
| | | | | | | | | | | | - 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
* Merge of branches/full-expr-4:xleroy2010-08-181-0/+365
- 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
generated by cgit (git 2.34.1) at 2024-05-19 17:01:47 +0000