Commits · e431dcf84d7e1a1106a501d53492b672c9d0b86e · CertiCompil / CompCert-KVX

Jan 07, 2008
- Function -> Definition (probleme de performance avec Coq8.1pl3) · e431dcf8
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  e431dcf8
Dec 08, 2007
- Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Compcert) · 3a84d95c
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@460 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  3a84d95c
Dec 06, 2007

Ajout find_symbol_not_nullptr; nettoyages · 64bacbbc

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

64bacbbc

Nov 13, 2007
- In Clight, revised handling of comparisons between pointers and 0 · b9eef999
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  b9eef999
Nov 03, 2007

Ajout de global_addresses_distinct · 3db50bce

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@445 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3db50bce

Oct 31, 2007
- Problemes d'alignement des variables globales et a l'interieur de leurs initialiseurs · fd04963d
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  fd04963d
- Simplification des Cconst_symbol: seules les versions 'signed' sont conservees · 108804d8
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@443 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  108804d8
- Simplification des Cconst_symbol: seules les versions 'signed' sont conservees · 636e4500
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  636e4500
Oct 30, 2007

Revu l'heuristique de linearisation · 5d742d80

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5d742d80

Oct 27, 2007
- Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG · e882493e
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  e882493e
Oct 17, 2007

Typo dans le pseudocode en commentaire · 7f6ac320

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@423 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7f6ac320

MAJ · 695fd6b6

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@422 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

695fd6b6

MAJ · 89234ade

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@421 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

89234ade

Relaxation de la regle d'evaluation Ecast · 0d2f4a41

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@420 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

0d2f4a41

Utilisation d'une monade avec types dependants pour garder trace des proprietes state_incr · 8a07279b
xleroy authored 17 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
8a07279b

Aug 28, 2007

Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les... · c48b9097

xleroy authored 17 years ago

Fusion de la branche restr-cminor.  En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements.  Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor.  Preuve de preservation semantique pour les programmes qui divergent.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

c48b9097

Aug 26, 2007

Ajout de common/Complements.v · 2b89ae94

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2b89ae94

Aug 06, 2007

Rendu le test lists.c plus interessant · eb5d2cee

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

eb5d2cee

Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles · 94aea060
xleroy authored 17 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
94aea060

Aug 05, 2007

Documentation · c0bc1466

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

c0bc1466

Aug 04, 2007

Deplacement du repertoire "papers" dans la hierarchie SVN · adc9e990

xleroy authored 17 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

adc9e990

Fusion des modifications faites sur les branches "tailcalls" et "smallstep". · 355b4abc

xleroy authored 17 years ago

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

355b4abc

Aug 03, 2007
- Version longue et mise a jour du papier sur le front-end (premier jet). · 22ff08b3
  blazy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  22ff08b3
Mar 23, 2007

Utilisation de Function · 21a429c6

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@210 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

21a429c6

Mar 05, 2007

Commentaires · 89dad2d4

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@184 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

89dad2d4

Importer OrderedPositive depuis Ordered.v · 4d0036db

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@183 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4d0036db

Mar 02, 2007

Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de... · c98440ca

xleroy authored 18 years ago

Suppression de lib/Sets.v, utilisation de FSet a la place.  Generalisation de Lattice pour utiliser une notion d'egalite possiblement differente de =.  Adaptation de Kildall et de ses utilisateurs en consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

c98440ca

Nettoyage · 28e7bce8

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@181 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

28e7bce8

Mettre les 2 demi-espaces dans 2 blocs separes · 8725f182

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@180 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8725f182

Preuve des 2 axiomes restants · a5ea703d

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@179 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

a5ea703d

Ajout lemmes utiles sur egalite decidable · 9b11be0d

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@178 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9b11be0d

Jan 03, 2007

Ajout operation eq dans PMap et IndexedMap · bec37242

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

bec37242

Nov 11, 2006

Petites adaptations pour Coq 8.1gamma · a3bc7b24

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

a3bc7b24

Oct 27, 2006

Ajout test mark&sweep GC · 7a333843

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@134 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7a333843

Oct 26, 2006

Ajout test stop&copy GC · ca285074

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@133 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

ca285074

Oct 23, 2006

Rapport d'erreur dans CIL · 23818138

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@130 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

23818138

Propagation des erreurs · c6dc421f

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

c6dc421f

Relaxation des contraintes sur les struct recursives · a543aeaf

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

a543aeaf

Location pour erreur sur le type de main() · ec553a83

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

ec553a83

Verification du type de retour de main() · 571a9c7b

xleroy authored 18 years ago

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

571a9c7b