Commits · a9621943087a5578c995d88b06f87c5158eb5d00 · CertiCompil / CompCert-KVX

Mar 29, 2009

Bug with overflow in line numbers · a9621943

xleroy authored 16 years ago

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

a9621943

Mar 28, 2009

Honor "static" modifier on C globals. · 3b8c7933

xleroy authored 16 years ago

Put "const" globals in read-only section.
Revised printing of rlwinm instruction.

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

3b8c7933

Mar 26, 2009

Update · a1d9acb0

xleroy authored 16 years ago

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

a1d9acb0

Added tail call optimization pass · 00b605a1

xleroy authored 16 years ago

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

00b605a1

Feb 27, 2009

Optimize redundant casts after memory loads · c90abe06

xleroy authored 16 years ago

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

c90abe06

New linearization heuristic · 72f346ba

xleroy authored 16 years ago

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

72f346ba

make install: ./ccomp au lieu de ../ccomp · 2837d6de

blazy authored 16 years ago

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

2837d6de

Feb 26, 2009
- Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >= 0' and 'x < 0'. · a745efa7
  xleroy authored 16 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@999 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  a745efa7
Jan 29, 2009

Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive... · 26fcc4db

xleroy authored 16 years ago

Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive file systems.  Replaced CList by CoqList and likewise for CString and CInt.  Removed useless references to CList in hand-written Caml code.

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

26fcc4db

Jan 11, 2009

Elimination of "alloc" instruction in Caml files and test files. · f6ecbb94
xleroy authored 16 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
f6ecbb94

- Added alignment constraints to memory loads and stores. · bb9d14a3

xleroy authored 16 years ago

- In Cminor and below, removed pointer validity check in semantics of 
  comparisons, so that evaluation of expressions is independent of
  memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.


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

bb9d14a3

Jan 07, 2009

Fixed unary minus · cd2449aa

xleroy authored 16 years ago

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

cd2449aa

Test for int/float conversions · 33a2f642

xleroy authored 16 years ago

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

33a2f642

Jan 05, 2009

Updates · deebc6fa

xleroy authored 16 years ago

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

deebc6fa

Endianness in tests · bd6a21e2

xleroy authored 16 years ago

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

bd6a21e2

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

Some cleanups · 7e18fbae

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