Commits · a24cfb086163ab359735392340acfe03e133be64 · CertiCompil / CompCert-KVX

Mar 08, 2010

Handling of volatile accesses through builtin functions. · a24cfb08

xleroy authored 15 years ago

Added support for processor-specific builtin functions.
Added some PowerPC instructions as builtins.
Updated #pragma section handling.


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

a24cfb08

Mar 07, 2010

Handling of builtins, continued. · c24a6527

xleroy authored 15 years ago

PrintCsyntax, PrintAsm: improve printing of float literals.


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

c24a6527

Revised treatment of builtins · 6a850311

xleroy authored 15 years ago

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

6a850311

Merge of the newmem and newextcalls branches: · a74f6b45

xleroy authored 15 years ago

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


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

a74f6b45

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
Suppressed Init_pointer, now useless. Improved printing of strings in generated .s · 1e24932c
xleroy authored 15 years ago
```
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1274 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
```
1e24932c

Detect struct assignment. Silence some warnings · 16e42ca8

xleroy authored 15 years ago

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

16e42ca8

Support for 'inline' modifier · f961ff40

xleroy authored 15 years ago

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

f961ff40

Updated raytracer test. Added SPASS test. · 6c196ec8

xleroy authored 15 years ago

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

6c196ec8

Getting rid of CIL · 93d89c2b

xleroy authored 15 years ago

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

93d89c2b

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

Mar 02, 2010

Protoized · 018edf2d

xleroy authored 15 years ago

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

018edf2d

Protoized · 31da663e

xleroy authored 15 years ago

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

31da663e

Function types didn't always degrade to pointers like they should. Introduced... · 1e700941

xleroy authored 15 years ago

Function types didn't always degrade to pointers like they should.  Introduced and used Csyntax.typeconv to address this issue and reduce the number of cases in the classify functions

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

1e700941

Wrong rlwinm generated for 'x mod 1' · 28e4632d

xleroy authored 15 years ago

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

28e4632d

Feb 17, 2010

Typo in Makefile · 47ff904d

xleroy authored 15 years ago

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

47ff904d

Reorganization test directory · 6224148f

xleroy authored 15 years ago

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

6224148f

3 more benchmarks · f9ebf19b

xleroy authored 15 years ago

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

f9ebf19b

Moved test harness C files here · 6f3a9afd

xleroy authored 15 years ago

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

6f3a9afd

Jan 31, 2010

Existence of behaviors · f6bdc196

xleroy authored 15 years ago

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

f6bdc196

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

Jan 25, 2010

Updated ARM asm printer · 3df67218

xleroy authored 15 years ago

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

3df67218

Updated ARM port · ed7f2503

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