Commits · 611e7b09253dbbb98e9cd4ca4e07a60b50e693fd · CertiCompil / CompCert-KVX

Jul 08, 2008

Fusion partielle de la branche contsem: · 611e7b09

xleroy authored 16 years ago

- semantiques a continuation pour Cminor et CminorSel
- goto dans Cminor

Suppression de backend/RTLbigstep.v, devenu inutile.


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

611e7b09

Jul 07, 2008
- Nettoyage du traitement des signatures au return dans LTL et LTLin · 0290650b
  xleroy authored 16 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  0290650b
May 31, 2008

Utilisation de intoffloatu. Ajout du cas int + ptr. · ea23f126

xleroy authored 16 years ago

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

ea23f126

May 30, 2008

Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs... · 72c5d592

xleroy authored 16 years ago

Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs vers des blocs differents!

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

72c5d592

Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore... · f4b41226

xleroy authored 16 years ago

Introduction de l'operation intuoffloat (float -> unsigned int).  Pas encore utilisee dans le front-end C.

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

f4b41226

Suppression de 'exten', inutilise · f77e0ade

xleroy authored 16 years ago

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

f77e0ade

Apr 19, 2008

Compilo C, preprocesseur, assembleur sont determines par configure et mis dans Makefile.config · 12332985
xleroy authored 16 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
12332985
Erreur dans la traduction d'un for lorsque la condition est complexe · c7a809ee
xleroy authored 16 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
c7a809ee

Impression des 'for' · d38d0487

xleroy authored 16 years ago

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

d38d0487

Detecter __builtin_xxx · 9fdd9361

xleroy authored 16 years ago

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

9fdd9361

Apr 17, 2008

Amelioration compilation des switch · 9e2f7e70

xleroy authored 16 years ago

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

9e2f7e70

Apr 16, 2008

Camlcoq.ml: interpret Caml's int32 as unsigned when converting to Integers.int · 3a34c435

xleroy authored 16 years ago

Cil2Csyntax.ml: terminating NUL character in strings within initialized data


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

3a34c435

Apr 15, 2008

Ajout du test vmach · c460156b

xleroy authored 16 years ago

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

c460156b

MAJ · 1231dacb

xleroy authored 16 years ago

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

1231dacb

Apr 13, 2008

Alignement de la pile dans PrintPPC · 795ae4b8

xleroy authored 16 years ago

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

795ae4b8

Apr 12, 2008

Revu le traitement de la 'red zone' en bas de la pile · 41ef4d52

xleroy authored 16 years ago

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

41ef4d52

Revu gestion retaddr et link dans Stacking · aaa49526

xleroy authored 16 years ago

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

aaa49526

Mar 27, 2008

Meilleure selection pour if ((a && b) != 0), etc · 845148de

xleroy authored 17 years ago

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

845148de

Mar 19, 2008

Revu removeproof · 68881dcd

xleroy authored 17 years ago

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

68881dcd

Nettoyages doc · 22d8a1d4

xleroy authored 17 years ago

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

22d8a1d4

Mar 04, 2008

Probleme echo -ne sur MacOS 10.5 · f85ac5c2

xleroy authored 17 years ago

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

f85ac5c2

Jan 28, 2008

Dates · 7a0378bd

xleroy authored 17 years ago

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

7a0378bd

Jan 27, 2008

Ajout license, README, copyright notices · 877b4347

xleroy authored 17 years ago

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

877b4347

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