Commits · ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab · CertiCompil / CompCert-KVX

Jan 25, 2010

xleroy authored 15 years ago

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

ed7f2503

Jan 13, 2010

Backtracking on commit 1220 · 307da4d1

xleroy authored 15 years ago

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

307da4d1

Jan 12, 2010

MAJ release 1.6 · 33a4bcf3

xleroy authored 15 years ago

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

33a4bcf3

MAJ Changes · 94484247

xleroy authored 15 years ago

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

94484247

Jan 08, 2010

ajout branche allocation de registres · a8c74400

blazy authored 15 years ago

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

a8c74400

Dec 16, 2009

Test result more reproducible · 283afabc

xleroy authored 15 years ago

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

283afabc

MAJ extraction after changes in Integers · 1cd87015

xleroy authored 15 years ago

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

1cd87015

MAJ Changes · 8d40eb31

xleroy authored 15 years ago

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

8d40eb31

Nov 19, 2009

Revised lib/Integers.v to make it parametric w.r.t. word size. · ef40c6d3

xleroy authored 15 years ago

Introduced Int.iwordsize and used it in place of "Int.repr 32" or
"Int.repr (Z_of_nat wordsize)".

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

ef40c6d3

Added support for jump tables. · cdf83055

xleroy authored 15 years ago

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

cdf83055

Unsupported: return/return type mismatches · d0ed98b8

xleroy authored 15 years ago

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

d0ed98b8

Nov 18, 2009

Cleaned up list_drop. · 01f1bf7a

xleroy authored 15 years ago

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

01f1bf7a

Nov 10, 2009
- More realistic treatment of jump tables: show the absence of overflow when accessing the table · 8ccc7f2f
  xleroy authored 15 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1172 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  8ccc7f2f
- Added support for jump tables in back end. · 74487f07
  xleroy authored 15 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  74487f07
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
- Use callee-save regs starting with R31/F31 and going down, like Diab does · e47dcb41
  xleroy authored 15 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1166 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  e47dcb41
- 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

Support Clight initializers of the form "int * x = &y;". · 033aa055

xleroy authored 15 years ago

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

033aa055

Oct 30, 2009
- Storing of single floats: must insert frsp instruction before store. (Temporary fix.) · 258a1fee
  xleroy authored 15 years ago
  
  git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
  258a1fee
Oct 25, 2009

Problem with MacOS X 10.6 · 20b484ea

xleroy authored 15 years ago

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

20b484ea

Sep 15, 2009

Problem with const enum initializers · 1ebccda6

xleroy authored 15 years ago

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

1ebccda6

Updated for 1.5 · 9534f739

xleroy authored 15 years ago

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

9534f739

Aug 28, 2009

Last updates for release 1.5. · 03b8970a

xleroy authored 15 years ago

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

03b8970a

Aug 27, 2009

Updated for release 1.5 · 82d24661

xleroy authored 15 years ago

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

82d24661

Remove "-ccopt -g" options: not really useful and causing problems with... · 71ad9090

xleroy authored 15 years ago

Remove "-ccopt -g" options: not really useful and causing problems with flexdll in the Win32/mingw port of Caml.


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

71ad9090

Aug 26, 2009

Coloringaux: make identifiers unique; special treatment of precolored · 0ba10d80

xleroy authored 15 years ago

  nodes a la Appel and George.
Maps: in PTree.combine, compress useless subtrees.
Lattice: more efficient implementation of LPMap.
Makefile: build profiling version


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

0ba10d80

Typo in doc · 15ac9e36

xleroy authored 15 years ago

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

15ac9e36

Aug 21, 2009

Stronger constant folding, esp. w.r.t. floats · d176dda2

xleroy authored 15 years ago

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

d176dda2

Aug 20, 2009

In generated Cminor functions, make sure local variables include · 17958d53

xleroy authored 15 years ago

all x used as destination of a call [x = f(args)]. This wasn't true before
if x was a global C#minor variable.

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

17958d53

Build bytecode version with debug symbols. · 5d2d2d27

xleroy authored 15 years ago

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

5d2d2d27

Aug 18, 2009

Updated Selection · 6d33055a

xleroy authored 15 years ago

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

6d33055a

Declaration of use_fused_mul, unused in this port but needed for extraction (I think) · 163395dc
xleroy authored 15 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1131 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
163395dc

Forgot to add some files · e860ffd6

xleroy authored 15 years ago

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

e860ffd6

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

"val_match_approx_increasing" moved from mach-dep part to mach-indep part. · 24a8dbb6
xleroy authored 15 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
24a8dbb6

Aug 17, 2009

Typo doc · f43399e0

xleroy authored 15 years ago

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

f43399e0

Refactoring of Constprop and Constpropproof into a machine-dependent part and... · a8fc4625

xleroy authored 15 years ago

Refactoring of Constprop and Constpropproof into a machine-dependent part and a machine-independent part.



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

a8fc4625

Refactored Selection.v and Selectionproof.v into a machine-dependent part + a... · 2199fd18

xleroy authored 15 years ago

Refactored Selection.v and Selectionproof.v into a machine-dependent part + a machine-independent part.


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

2199fd18

Aug 16, 2009

Cil2Csyntax: added goto and labels; added assignment between structs · 4b119d6f

xleroy authored 15 years ago

Kildall: simplified the interface
Constprop, CSE, Allocation, Linearize: updated for the new Kildall
RTL, LTL: removed the well-formedness condition on the CFG, 
  it is no longer necessary with the new Kildall and it is problematic
  for validated optimizations.
Maps: more efficient implementation of PTree.fold.


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

4b119d6f