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
...
*
MAJ
xleroy
2008-04-15
2
-147
/
+133
*
Alignement de la pile dans PrintPPC
xleroy
2008-04-13
2
-12
/
+16
*
Revu le traitement de la 'red zone' en bas de la pile
xleroy
2008-04-12
8
-58
/
+65
*
Revu gestion retaddr et link dans Stacking
xleroy
2008-04-12
17
-934
/
+1032
*
Meilleure selection pour if ((a && b) != 0), etc
xleroy
2008-03-27
2
-27
/
+277
*
Revu removeproof
xleroy
2008-03-19
4
-26
/
+50
*
Nettoyages doc
xleroy
2008-03-19
2
-15
/
+6
*
Probleme echo -ne sur MacOS 10.5
v1.2
xleroy
2008-03-04
1
-0
/
+14
*
Dates
xleroy
2008-01-28
1
-1
/
+1
*
Ajout license, README, copyright notices
xleroy
2008-01-27
110
-4
/
+2027
*
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
[prev]
[next]