(i.e. not preceded by another bit field).


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

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

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

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

Globalenvs.v: used drop_perm to set appropriate permissions on global variables
  (Notempty if volatile; Readable if readonly; Writable otherwise)


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

Heuristic to choose test data.


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

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

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

cparser/Elab.ml: tolerate changes in qualifiers in ?:
cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static.


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

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

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

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

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

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

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

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



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

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

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

Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of reading a small unsigned bitfield

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

  as bitwise operations rather than arithmetic ones.
CastOptimproof: fixed for ARM port.
Other files: adapted to changes in Integers.


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

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

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

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

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

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



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

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

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

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

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

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

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

AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
  and a machine-dependent part (ARCH/SYS/Conventions1).


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

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

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

*/PrintAsm.ml: watch out for large stack frames in Pallocframe.


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

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

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

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

- Revised handling of volatile reads: the execution environment
  dictates the value read, via the trace of events.


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

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