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
/
backend
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
Revu traitement des variables globales dans AST.program et dans Globalenvs.
xleroy
2006-09-05
11
-18
/
+18
*
Revu la repartition des sources Coq en sous-repertoires
xleroy
2006-09-04
9
-8171
/
+0
*
Fusion de la branche "traces":
xleroy
2006-09-04
53
-8018
/
+4666
*
Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de
xleroy
2006-07-11
3
-165
/
+149
*
MAJ suite aux changements dans Cminorgen
xleroy
2006-06-08
1
-3
/
+7
*
Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kind
xleroy
2006-06-06
3
-27
/
+61
*
Optimisation des casts (idempotence, etc)
xleroy
2006-06-05
2
-51
/
+121
*
Ajout construction Sswitch dans Cminor
xleroy
2006-06-05
1
-8
/
+39
*
Ajout construction Sswitch dans Cminor
xleroy
2006-06-05
3
-9
/
+103
*
Revu gestion des variables globales dans Csharpminor
xleroy
2006-06-02
3
-274
/
+457
*
Dans Cminor et Csharpminor: suppression de stmtlist, ajout de Sskip, Sseq.
xleroy
2006-04-06
9
-349
/
+247
*
Suppression de stmtlist et de exec_stmtlist.
xleroy
2006-04-06
1
-45
/
+31
*
PL: Un mot-cle Proof qui n'a rien a faire la...
letouzey
2006-02-16
1
-1
/
+0
*
Initial import of compcert
xleroy
2006-02-09
55
-0
/
+40577
[prev]