Commits · 4c8a550fae641115170e4fc9c1b1292834e0c6c0 · CertiCompil / CompCert-KVX

Jul 31, 2008

Flag to turn on/off the recognition of fused multiply-add and multiply-sub · 4c8a550f
xleroy authored 16 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
4c8a550f

xleroy authored 16 years ago

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

99294ec7

Update test results · 1bf0ee95

xleroy authored 16 years ago

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

1bf0ee95

Jul 27, 2008

MAJ documentation · cab28a53

xleroy authored 16 years ago

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

cab28a53

Jul 25, 2008

Simplification de la semantique de LTL et LTLin. Les details lies aux... · b5325808

xleroy authored 16 years ago

Simplification de la semantique de LTL et LTLin.  Les details lies aux conventions d'appel sont maintenant geres de maniere plus locale dans la passe Reload.

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

b5325808

Augmenter le temps d'execution par defaut · 65a29b66

xleroy authored 16 years ago

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

65a29b66

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