aboutsummaryrefslogtreecommitdiffstats
BranchCommit messageAuthorAge
masterUpdate verilog back end with new x86 changesYann Herklotz13 months
dev/michalisMerge branch 'master' into dev/michalisYann Herklotz3 years
inl-cse-constAdd switch of passYann Herklotz3 years
aarch64AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.leroy5 years
no-pervasivesClarify "open" statementsXavier Leroy5 years
floatofintux86 branchless implementation of float -> unsigned int32 conversionXavier Leroy5 years
conditional-moveIf-conversion optimization for CminorXavier Leroy5 years
FPcompUpdate the proofs after rebaseXavier Leroy5 years
 
TagDownloadAuthorAge
v3.10compcert-3.10.tar.gz  compcert-3.10.zip  Xavier Leroy3 years
v3.9compcert-3.9.tar.gz  compcert-3.9.zip  Xavier Leroy3 years
v3.8compcert-3.8.tar.gz  compcert-3.8.zip  Xavier Leroy4 years
v3.7compcert-3.7.tar.gz  compcert-3.7.zip  Xavier Leroy4 years
v3.6compcert-3.6.tar.gz  compcert-3.6.zip  Xavier Leroy5 years
v3.5compcert-3.5.tar.gz  compcert-3.5.zip  Xavier Leroy5 years
v3.4compcert-3.4.tar.gz  compcert-3.4.zip  Xavier Leroy6 years
v3.3compcert-3.3.tar.gz  compcert-3.3.zip  Xavier Leroy6 years
v3.2compcert-3.2.tar.gz  compcert-3.2.zip  Bernhard Schommer6 years
v3.1compcert-3.1.tar.gz  compcert-3.1.zip  Xavier Leroy7 years
[...]
 
AgeCommit messageAuthorFilesLines
2008-03-04Probleme echo -ne sur MacOS 10.5v1.2xleroy1-0/+14
2008-01-28Datesxleroy1-1/+1
2008-01-27Ajout license, README, copyright noticesxleroy110-4/+2027
2008-01-07Function -> Definition (probleme de performance avec Coq8.1pl3)xleroy1-1/+1
2007-12-08Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...xleroy1-6/+363
2007-12-06Ajout find_symbol_not_nullptr; nettoyagesxleroy1-39/+71
2007-11-13In Clight, revised handling of comparisons between pointers and 0xleroy4-39/+39
2007-11-03Ajout de global_addresses_distinctxleroy1-16/+75
2007-10-31Problemes d'alignement des variables globales et a l'interieur de leurs initi...xleroy7-166/+234
2007-10-31Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy1-4/+2
[...]
 
Clone
https://git.ymhg.org/compcert
ssh://git@git.ymhg.org:compcert