aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
Commit message (Expand)AuthorAgeFilesLines
* Fix tracing options for clightgen.Bernhard Schommer2019-07-151-10/+23
* Correct typo in Clightnorm.ml (#285)Alix Trieu2019-03-271-1/+1
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-202-4/+21
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-15/+18
* Share code for common options.Bernhard Schommer2018-01-291-70/+15
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-01-171-3/+9
|\
| * 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
* | Added missing help and common options.Bernhard Schommer2018-01-171-1/+15
|/
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-111-20/+1
* Added option -o to clightgen.Bernhard Schommer2018-01-111-5/+47
* Add riscv and attributes to ClightgenBernhard Schommer2018-01-101-0/+4
* Minor improvements.Bernhard Schommer2018-01-101-2/+2
* Change README to markdown.Bernhard Schommer2018-01-101-15/+14
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-031-1/+1
* Use quoted strings in clightgen.Bernhard Schommer2018-01-021-22/+24
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-2/+2
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-282-16/+6
* Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-152-13/+33
* clightgen: add option -normalize to ensure that memory loads never occur "dee...Xavier Leroy2017-06-122-2/+177
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-281-3/+8
* 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
* | Additional test for color output.Bernhard Schommer2016-08-051-10/+10
|/
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
* Added version string to Clightgen.Bernhard Schommer2016-05-241-2/+14
* Escape all newlines.Bernhard Schommer2016-05-241-5/+5
* Moved shared frontend code in own file.Bernhard Schommer2016-05-241-161/+28
* 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
* | Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
|/
* Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
* 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
* 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
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-233-17/+33
generated by cgit (git 2.34.1) at 2024-06-01 10:46:43 +0000