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