aboutsummaryrefslogtreecommitdiffstats
path: root/test/export
Commit message (Collapse)AuthorAgeFilesLines
* test/export: use the standard headers from ../../runtime/includeXavier Leroy2022-09-231-1/+1
| | | | Just like in the other test/ directories.
* Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-229-0/+1034
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.