aboutsummaryrefslogtreecommitdiffstats
path: root/export/Clightdefs.v
Commit message (Collapse)AuthorAgeFilesLines
* Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-221-243/+4
| | | | | | | | | 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-221-0/+304
Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/