aboutsummaryrefslogtreecommitdiffstats
path: root/export
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into towards_3.10David Monniaux2021-09-273-0/+3
|
* Update export/README.mdXavier Leroy2021-09-221-18/+18
|
* Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-228-255/+588
| | | | | | | | | As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output.
* Refactor clightgenXavier Leroy2021-09-227-0/+1350
Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/