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
*
Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...
xleroy
2007-03-02
21
-1010
/
+594
*
Nettoyage
xleroy
2007-03-02
1
-1
/
+0
*
Mettre les 2 demi-espaces dans 2 blocs separes
xleroy
2007-03-02
1
-9
/
+10
*
Preuve des 2 axiomes restants
xleroy
2007-03-02
1
-2
/
+17
*
Ajout lemmes utiles sur egalite decidable
xleroy
2007-03-02
1
-0
/
+31
*
Ajout operation eq dans PMap et IndexedMap
xleroy
2007-01-03
1
-0
/
+10
*
Petites adaptations pour Coq 8.1gamma
xleroy
2006-11-11
8
-20
/
+27
*
Ajout test mark&sweep GC
xleroy
2006-10-27
5
-2
/
+439
*
Ajout test stop© GC
xleroy
2006-10-26
3
-1
/
+404
*
Rapport d'erreur dans CIL
xleroy
2006-10-23
1
-1
/
+3
*
Propagation des erreurs
xleroy
2006-10-23
1
-20
/
+94
*
Relaxation des contraintes sur les struct recursives
xleroy
2006-10-23
2
-14
/
+10
*
Location pour erreur sur le type de main()
xleroy
2006-10-23
1
-1
/
+2
*
Verification du type de retour de main()
xleroy
2006-10-23
1
-10
/
+8
*
Lever la restriction sur les fonctions externes, restriction qui exigeait que...
xleroy
2006-10-22
19
-167
/
+267
*
Meilleur traitement des fonctions forward declared. Ajout d'un warning sur l...
xleroy
2006-10-22
1
-0
/
+16
*
Ajout et utilisation de compcert_stdio.h
xleroy
2006-10-22
6
-6
/
+210
*
Resolution d'un probleme (cf. big endian), et
blazy
2006-10-20
11
-20
/
+12
*
Ajout du banc de tests de CCured (Olden benchmark suite, cf.
blazy
2006-10-20
202
-0
/
+12593
*
cleaning...
lrg
2006-10-20
1
-2
/
+1
*
interpreter for "little"
lrg
2006-10-20
16
-0
/
+1336
*
Meilleure compilation de la negation booleenne
xleroy
2006-09-19
5
-7
/
+15
*
Simplification de Cminor: les affectations de variables locales ne sont
xleroy
2006-09-18
11
-981
/
+792
*
Suite des stubs variadiques.
xleroy
2006-09-17
1
-16
/
+13
*
Preprocesser en definissant __ppc__ (utile pour l'emulation MacOSX/Intel)
xleroy
2006-09-17
1
-1
/
+1
*
Nettoyages
xleroy
2006-09-17
4
-18
/
+16
*
Revu generation de stubs pour les fonctions variadiques
xleroy
2006-09-17
1
-28
/
+106
*
typo in comment
xleroy
2006-09-17
1
-1
/
+1
*
Type unrolling in struct and union fields
xleroy
2006-09-17
1
-5
/
+30
*
Davantage de tests
xleroy
2006-09-17
33
-33
/
+3010
*
Bug dans le traitement des fonctions variadiques.
xleroy
2006-09-17
1
-25
/
+54
*
Meilleur message de debug dans le cas Icall
xleroy
2006-09-17
1
-6
/
+15
*
Ajout de Init_pointer (experimental)
xleroy
2006-09-17
4
-4
/
+61
*
Const.prop dans la taille des tableaux. Tolerer (avec warning) les declarati...
xleroy
2006-09-16
1
-5
/
+9
*
Ajout du test lists
xleroy
2006-09-11
2
-2
/
+57
*
Utiliser l'extension .light.c au lieu de .clight
xleroy
2006-09-11
1
-1
/
+1
*
Typo dans impression structs
xleroy
2006-09-11
1
-1
/
+1
*
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
[next]