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
*
Function -> Definition (probleme de performance avec Coq8.1pl3)
xleroy
2008-01-07
1
-1
/
+1
*
Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...
xleroy
2007-12-08
1
-6
/
+363
*
Ajout find_symbol_not_nullptr; nettoyages
xleroy
2007-12-06
1
-39
/
+71
*
In Clight, revised handling of comparisons between pointers and 0
xleroy
2007-11-13
4
-39
/
+39
*
Ajout de global_addresses_distinct
xleroy
2007-11-03
1
-16
/
+75
*
Problemes d'alignement des variables globales et a l'interieur de leurs initi...
xleroy
2007-10-31
7
-166
/
+234
*
Simplification des Cconst_symbol: seules les versions 'signed' sont conservees
xleroy
2007-10-31
1
-4
/
+2
*
Simplification des Cconst_symbol: seules les versions 'signed' sont conservees
xleroy
2007-10-31
3
-79
/
+59
*
Revu l'heuristique de linearisation
xleroy
2007-10-30
1
-46
/
+36
*
Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG
xleroy
2007-10-27
9
-197
/
+363
*
Typo dans le pseudocode en commentaire
xleroy
2007-10-17
1
-1
/
+1
*
MAJ
xleroy
2007-10-17
1
-107
/
+107
*
MAJ
xleroy
2007-10-17
2
-5
/
+6
*
Relaxation de la regle d'evaluation Ecast
xleroy
2007-10-17
2
-4
/
+4
*
Utilisation d'une monade avec types dependants pour garder trace des propriet...
xleroy
2007-10-17
3
-556
/
+461
*
Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...
xleroy
2007-08-28
33
-3523
/
+4572
*
Ajout de common/Complements.v
xleroy
2007-08-26
6
-2
/
+674
*
Rendu le test lists.c plus interessant
xleroy
2007-08-06
1
-4
/
+30
*
Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles
xleroy
2007-08-06
12
-514
/
+548
*
Documentation
xleroy
2007-08-05
17
-352
/
+584
*
Deplacement du repertoire "papers" dans la hierarchie SVN
xleroy
2007-08-04
17
-6605
/
+0
*
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
xleroy
2007-08-04
109
-23374
/
+18742
*
Version longue et mise a jour du papier sur le front-end (premier jet).
blazy
2007-08-03
17
-0
/
+6605
*
Utilisation de Function
xleroy
2007-03-23
1
-51
/
+13
*
Commentaires
xleroy
2007-03-05
1
-4
/
+4
*
Importer OrderedPositive depuis Ordered.v
xleroy
2007-03-05
1
-30
/
+1
*
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
[next]