aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/ExportClight.ml
Commit message (Expand)AuthorAgeFilesLines
* better failDavid Monniaux2021-09-271-1/+1
* fix clightgenDavid Monniaux2021-09-271-0/+3
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-5/+8
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-2/+2
* Use exact arithmetic for printing positive numbersXavier Leroy2020-09-221-52/+56
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-0/+1
* clightgen: fix the printing of annotationsXavier Leroy2020-06-051-59/+8
* clightgen -short-idents : do not use $"xxx" notation everXavier Leroy2020-06-011-1/+1
* Add a canonical encoding of identifiers as numbers and use it in clightgen (#...Xavier Leroy2020-05-191-14/+21
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-2/+10
* clightgen: sanitize names of functions and global variablesXavier Leroy2019-10-281-4/+4
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-201-3/+19
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
* Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
* Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-2/+2
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-281-5/+4
* Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-151-8/+9
* 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
* 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
* | Cleanup of Clightgen code.Bernhard Schommer2016-03-101-42/+39
|/
* Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
* 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
* 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
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-231-14/+26
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+0
* Merge of the "alignas" branch.xleroy2013-10-051-4/+9
* Merge of the "princeton" branch:xleroy2013-06-161-4/+54
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-1/+19
* List.iteri not in OCaml < 4.00, better not use it.xleroy2013-04-081-2/+9
* Update clightgen to changes in Camlcoq and in AST.xleroy2013-03-201-14/+32
* Put clighgen files in exportclight/xleroy2013-01-051-0/+503
generated by cgit (git 2.34.1) at 2024-05-09 06:01:14 +0000