index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
test
/
clightgen
Commit message (
Expand
)
Author
Age
Files
Lines
*
Add support to clightgen for generating Csyntax AST as .v files
Xavier Leroy
2021-09-22
7
-1022
/
+0
*
Refactor clightgen
Xavier Leroy
2021-09-22
1
-1
/
+1
*
clightgen: handle empty names given to padding bit fields
Xavier Leroy
2021-09-15
1
-0
/
+13
*
"macosx" is now called "macos"
Xavier Leroy
2021-01-18
1
-1
/
+1
*
Better "make clean"
Xavier Leroy
2020-11-01
1
-1
/
+1
*
Test clightgen with -short-idents and -normalize options
Xavier Leroy
2020-09-22
1
-0
/
+6
*
Support the use of already-installed MenhirLib and Flocq libraries
Xavier Leroy
2020-09-21
1
-2
/
+6
*
Improve portability of the test for annotations inclightgen
Xavier Leroy
2020-06-05
2
-0
/
+4
*
clightgen: fix the printing of annotations
Xavier Leroy
2020-06-05
1
-0
/
+6
*
clightgen: sanitize names of functions and global variables
Xavier Leroy
2019-10-28
1
-0
/
+12
*
Clean .foo.aux files created by coqc
Xavier Leroy
2018-07-10
1
-1
/
+1
*
Don't depend on ../../clightgen
Xavier Leroy
2018-06-02
1
-3
/
+3
*
Add tests for clightgen
Xavier Leroy
2018-06-01
4
-0
/
+977