compcert - CompCert fork with minor modifications for Vericert.

Branch	Commit message	Author	Age
master	Update verilog back end with new x86 changes	Yann Herklotz	13 months
dev/michalis	Merge branch 'master' into dev/michalis	Yann Herklotz	3 years
inl-cse-const	Add switch of pass	Yann Herklotz	3 years
aarch64	AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}	xavier.leroy	5 years
no-pervasives	Clarify "open" statements	Xavier Leroy	5 years
floatofintu	x86 branchless implementation of float -> unsigned int32 conversion	Xavier Leroy	5 years
conditional-move	If-conversion optimization for Cminor	Xavier Leroy	5 years
FPcomp	Update the proofs after rebase	Xavier Leroy	5 years

Tag	Download	Author	Age
v3.10	compcert-3.10.tar.gz compcert-3.10.zip	Xavier Leroy	2 years
v3.9	compcert-3.9.tar.gz compcert-3.9.zip	Xavier Leroy	3 years
v3.8	compcert-3.8.tar.gz compcert-3.8.zip	Xavier Leroy	4 years
v3.7	compcert-3.7.tar.gz compcert-3.7.zip	Xavier Leroy	4 years
v3.6	compcert-3.6.tar.gz compcert-3.6.zip	Xavier Leroy	5 years
v3.5	compcert-3.5.tar.gz compcert-3.5.zip	Xavier Leroy	5 years
v3.4	compcert-3.4.tar.gz compcert-3.4.zip	Xavier Leroy	6 years
v3.3	compcert-3.3.tar.gz compcert-3.3.zip	Xavier Leroy	6 years
v3.2	compcert-3.2.tar.gz compcert-3.2.zip	Bernhard Schommer	6 years
v3.1	compcert-3.1.tar.gz compcert-3.1.zip	Xavier Leroy	7 years
[...]

Age	Commit message	Author	Files	Lines
2019-08-31	AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}aarch64	xavier.leroy	2	-4/+4
2019-08-23	Offset out of range for ldp/stp instructions	xavier.leroy	1	-1/+3
2019-08-17	Fix compile for architectures other than AArch64 (#192)	Bernhard Schommer	6	-16/+16
2019-08-08	Test for the compilation of floating-point literals	Xavier Leroy	3	-1/+562
2019-08-08	AArch64 port	Xavier Leroy	48	-87/+14874
2019-08-07	Relax lemma Val.zero_ext_and and add Val.zero_ext_andl	Xavier Leroy	1	-2/+10
2019-08-07	Factor out endianness determination between tests	Xavier Leroy	4	-30/+14
2019-08-07	ndfun: add support for guards on patterns	Xavier Leroy	1	-5/+16
2019-08-07	More lemmas about powers of 2	Xavier Leroy	1	-0/+14
2019-08-07	Errors: fixed a loop in tactic MonadInv	Xavier Leroy	1	-1/+1
[...]

Clone
https://git.ymhg.org/compcert
ssh://git@git.ymhg.org:compcert