aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'towards_2.10' of ../towards_3.10 into kvx-workDavid Monniaux2021-09-304-716/+0
|\
| * Merge remote-tracking branch 'origin/kvx-work' into towards_3.10David Monniaux2021-09-271-0/+559
| |\
| * | Refactor clightgenXavier Leroy2021-09-225-1300/+0
| * | clightgen: handle empty names given to padding bit fieldsXavier Leroy2021-09-151-16/+15
| * | Native support for bit fields (#400)Xavier Leroy2021-08-221-1/+30
| * | Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-084-16/+20
| * | Update the output of clightgen to pick the `$` notation from its new placeXavier Leroy2021-04-231-1/+3
| * | Move `$` notation in submodule `ClightNotations` and scope `clight_scope`Xavier Leroy2021-04-231-11/+23
* | | 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-014-28/+46
|/
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-2/+2
* Add `string_of_ident` conversionXavier Leroy2020-10-121-0/+110
* Use exact arithmetic for printing positive numbersXavier Leroy2020-09-221-52/+56
* Fix computation of next temporary in -canonical-idents modeXavier Leroy2020-09-221-1/+12
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-0/+1
* clightgen: fix the printing of annotationsXavier Leroy2020-06-051-59/+8
* clightgen: fix usage messageXavier Leroy2020-06-011-2/+2
* 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-193-17/+128
* 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 -dclight: print function parameters correctlyXavier Leroy2019-09-161-1/+1
* 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
|/