Commits · 54cba6d4cae1538887f296a62be1c99378fe0916 · CertiCompil / CompCert-KVX

Mar 03, 2010

Suppressed -fall-extensions option, too dangerous wrt flonglong · 54cba6d4
xleroy authored 15 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1275 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
54cba6d4

Switching to the new C parser/elaborator/simplifier · 891377ce

xleroy authored 15 years ago

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

891377ce

Jan 27, 2010

Revised handling of #pragma section and small data areas · 87ada413

xleroy authored 15 years ago

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

87ada413

Nov 03, 2009

PowerPC/EABI port: preliminary support for #pragma section and · 0486654f

xleroy authored 15 years ago

  #pragma use_section.
Some clean-ups in Cil2Csyntax.
Separate mach-dep parts of extraction/extraction.v into
   <arch>/extractionMachdep.v


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

0486654f

Nov 02, 2009
- Simplified the treatment of the PowerPC small data area; now more specific to the Diab toolchain. · 5d84e686
  xleroy authored 15 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1165 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  5d84e686
Nov 01, 2009

Preliminary support for small data area in PowerPC port. · 3ccc9367

xleroy authored 15 years ago

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

3ccc9367

Aug 18, 2009

No '\n' in Coq strings... · 22d65c59

xleroy authored 15 years ago

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

22d65c59

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

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
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
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

Aug 06, 2007
- Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles · 94aea060
  xleroy authored 17 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  94aea060