aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
Commit message (Collapse)AuthorAgeFilesLines
* Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
|
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-1/+6
|
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-1/+3
|\
| * Implement support for big endian arm targets.Bernhard Schommer2016-08-051-1/+3
| | | | | | | | | | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* | Additional test for color output.Bernhard Schommer2016-08-051-10/+10
|/ | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
|
* Added version string to Clightgen.Bernhard Schommer2016-05-241-2/+14
| | | | | | Clightgen now also prints a version string. Also the CompCert version string is now similar in both modes. Bug 18768.
* Escape all newlines.Bernhard Schommer2016-05-241-5/+5
| | | | Bug 18768.
* Moved shared frontend code in own file.Bernhard Schommer2016-05-241-161/+28
| | | | | | | Clightgen and CompCert share the code for preprocessing as well as parsing C files. The code as well as command line switches is moved in the new module Frontend. Bug 18768
* bug 18004, fix file extensions for dparse optionMichael Schmidt2016-04-251-1/+1
|
* Also refactor clightgen to work with new warnings. Bug 18394Bernhard Schommer2016-03-231-6/+6
|
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-0/+2
|\
| * Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-0/+2
| |
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-152-27/+27
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
|/ | | | | Removed unused code and code generating warnings. Bug 18394
* Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
| | | | clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
* clightgen: update to recent change -fstruct-return/-fstruct-passingXavier Leroy2015-12-191-4/+7
|
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-202-8/+8
|
* 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.
* Upgrade to reflect changes in type external_function.Xavier Leroy2015-10-111-4/+2
|
* Update clightgen w.r.t. teh calling_conventions record (new field cc_unproto).Xavier Leroy2015-08-171-1/+2
|
* Update clightgen w.r.t. EF_inline_asm (type of the clobber list).Xavier Leroy2015-08-171-1/+6
|
* Update clightgen to the new annotations and the new inline asm.Xavier Leroy2015-04-232-25/+10
|
* Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-203-232/+151
|
* Refactoring in the printing of FP numbers.Xavier Leroy2014-09-241-8/+2
|
* Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc).Xavier Leroy2014-09-241-7/+20
|
* Merge of "newspilling" branch:xleroy2014-07-231-3/+3
| | | | | | | | | | | | | | | - 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
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-233-17/+33
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+0
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-052-14/+27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* One more copyright header update.xleroy2013-06-171-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update LICENSE file and headers for dual-licensed files.xleroy2013-06-171-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:xleroy2013-06-161-4/+54
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatedxleroy2013-04-301-3/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2219 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-202-1/+22
| | | | | | | | | 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
* List.iteri not in OCaml < 4.00, better not use it.xleroy2013-04-081-2/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update clightgen to changes in Camlcoq and in AST.xleroy2013-03-202-15/+33
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Put clighgen files in exportclight/xleroy2013-01-054-0/+872
Short doc in exportclight/README git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-28 21:35:22 +0000