Commits · 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 · CertiCompil / CompCert-KVX

Dec 29, 2008

Extract Coq lists to Caml lists. · 1bce6b0f

xleroy authored 16 years ago

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

1bce6b0f

Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext. · 12421d71

xleroy authored 16 years ago

lib/Integers.v: added more properties for ARM port.
lib/Coqlib.v: added more properties for division and powers of 2.

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

12421d71

Dec 21, 2008
- Revised back-end so that only 2 integer registers are reserved for reloading. · dc4bed2c
  xleroy authored 16 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@925 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  dc4bed2c
Sep 27, 2008

Clight: ajout Econdition, suppression Eindex. · ec6d00d9

xleroy authored 16 years ago

caml/PrintCsyntax.ml: afficher les formes a[b] et a->fld.



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

ec6d00d9

Aug 11, 2008

Update for release 1.3 · 2cf153d6

xleroy authored 16 years ago

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

2cf153d6

New file · 9679d3e6

xleroy authored 16 years ago

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

9679d3e6

Aug 09, 2008

Update · 048c1ddb

xleroy authored 16 years ago

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

048c1ddb

Changes 1.2 -> 1.3 · 6cc29f79

xleroy authored 16 years ago

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

6cc29f79

Ajout nouveaux tests · 285f5bec

xleroy authored 16 years ago

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

285f5bec

Aug 01, 2008

Plus besoin de rectifier les URL invalides · a83f0c17

xleroy authored 16 years ago

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

a83f0c17

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

Added Slabel, Sgoto · 99294ec7

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