aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/ExportClight.ml
Commit message (Collapse)AuthorAgeFilesLines
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-201-3/+19
| | | | | Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info. Closes: #226.
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
| | | | Added types for global_definitions in order to avoid problems with implicit parameters. This should fix issue 215
* Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
| | | | This should fix issue 216 and also allows it to print 64 bit offsets.
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-2/+2
| | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-281-5/+4
| | | | | Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert. Remove 'Require Export' from Clightdefs as suggested in issue #199.
* Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-151-8/+9
| | | | | | The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196. The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-281-3/+8
|
* Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
|
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
|
* Escape all newlines.Bernhard Schommer2016-05-241-5/+5
| | | | Bug 18768.
* 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-151-25/+25
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Cleanup of Clightgen code.Bernhard Schommer2016-03-101-42/+39
|/ | | | | 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.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-6/+6
|
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-13/+13
| | | | | | | | | | 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-231-24/+9
|
* Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-201-132/+38
|
* 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-231-14/+26
| | | | 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-051-4/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 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
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-1/+19
| | | | | | | | | 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-201-14/+32
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Put clighgen files in exportclight/xleroy2013-01-051-0/+503
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-26 18:15:40 +0000