Commits · bcc49e9df3e1885fcdf6e7a082f9101a323fb39c · CertiCompil / CompCert-KVX

Jan 04, 2009
- Cminor, CminorSel: removed useless premises in rules for Sreturn · bcc49e9d
  xleroy authored 16 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@938 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  bcc49e9d
Jan 02, 2009

xleroy authored 16 years ago

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

7e18fbae

Wrong dependencies · 322dc1ce

xleroy authored 16 years ago

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

322dc1ce

Jan 01, 2009

Continuation of ARM port. · 2245717b

xleroy authored 16 years ago

Cleaned up Makefile and SVN properties.


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

2245717b

Dec 31, 2008

Cleanup · 58fca75f

xleroy authored 16 years ago

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

58fca75f

Continuation of PowerPC/EABI port · 7cf9ed0e

xleroy authored 16 years ago

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

7cf9ed0e

Turn off generation of libcil.a, which is not correct with OCaml 3.11 · 831c5fdf
xleroy authored 16 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@932 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
831c5fdf
Removed vfprintf, because it was causing portability problems · c79395a8
xleroy authored 16 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@931 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
c79395a8

Dec 30, 2008

Reorganized the development, modularizing away machine-dependent parts. · 6d25b4f3

xleroy authored 16 years ago

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


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

6d25b4f3

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