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
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
Eviter de caster les fonctions directement dans le cas variadique, gcc dit qu...
xleroy
2006-09-11
1
-4
/
+1
*
Suppression des casts systematiques vers unsigned int dans les comparaisons d...
xleroy
2006-09-11
1
-9
/
+65
*
Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure...
xleroy
2006-09-11
7
-77
/
+82
*
Code de timing
xleroy
2006-09-11
1
-0
/
+26
*
MAJ suite ajouts dans Kildall. Compiler en code natif par defaut
xleroy
2006-09-11
2
-11
/
+29
*
Meilleure representation des worklists dans l'algo de Kildall
xleroy
2006-09-11
4
-68
/
+209
*
Encore une eta-expansion intempestive
xleroy
2006-09-11
1
-4
/
+23
*
Traiter les initialisations x = NULL
xleroy
2006-09-08
1
-0
/
+2
*
MAJ
xleroy
2006-09-08
1
-2
/
+2
*
Suite de l'adaptation du front-end CIL
xleroy
2006-09-08
4
-267
/
+325
*
MAJ des tests C
xleroy
2006-09-08
8
-61
/
+1082
*
Stocker l'adresse de retour a l'offset 12 au lieu de l'offset 4 pour meilleur...
xleroy
2006-09-08
8
-19
/
+19
*
Integration du front-end CIL developpe par Thomas Moniot
xleroy
2006-09-07
22
-119
/
+2688
*
Permettre les casts entre types de fonction
xleroy
2006-09-06
2
-13
/
+21
*
Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)
xleroy
2006-09-06
3
-10
/
+21
*
Ajout de dependances dans extraction/Makefile
tristan
2006-09-06
3
-24
/
+32
*
MAJ
xleroy
2006-09-06
2
-2
/
+4
*
Definition redondante
xleroy
2006-09-06
1
-5
/
+0
*
Revu traitement des variables globales dans AST.program et dans Globalenvs.
xleroy
2006-09-05
23
-468
/
+538
*
Ignorer les .vo dans cfrontend et common
xleroy
2006-09-04
0
-0
/
+0
*
Ignorer les .vo dans cfrontend et common
xleroy
2006-09-04
0
-0
/
+0
*
Convenience command
xleroy
2006-09-04
1
-0
/
+4
*
Revu la repartition des sources Coq en sous-repertoires
xleroy
2006-09-04
12
-67
/
+70
*
Fusion de la branche "traces":
xleroy
2006-09-04
88
-8418
/
+11331
*
Ajout d'un type-checker (non certifie) pour Cminor
xleroy
2006-07-17
6
-17
/
+397
*
Declaration des variables avec .comm
xleroy
2006-07-11
1
-3
/
+1
*
Ajout de fabs
xleroy
2006-07-11
1
-0
/
+1
*
Cast des litteraux de chaine en unsigned char *
xleroy
2006-07-11
2
-12
/
+12
*
Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de
xleroy
2006-07-11
3
-165
/
+149
*
Version C des tests Cminor
xleroy
2006-06-29
8
-0
/
+1339
*
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
*
Suppression de stmtlist dans Cminor
xleroy
2006-04-06
2
-6
/
+6
*
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
*
Renommage List -> CList lors de l'extraction
xleroy
2006-03-09
6
-229
/
+231
*
PL: Un mot-cle Proof qui n'a rien a faire la...
letouzey
2006-02-16
1
-1
/
+0
*
Properties
xleroy
2006-02-10
0
-0
/
+0
*
MAJ fichier ppal
xleroy
2006-02-09
1
-63
/
+63
*
Nettoyages
xleroy
2006-02-09
3
-75293
/
+4
*
Initial import of compcert
xleroy
2006-02-09
109
-0
/
+134574
[prev]