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@1500 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 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

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

*/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@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

wrong because of +0.0 / -0.0.  
Adapted Clight semantics accordingly.  (Truth value of a float is
defined by comparison Float.cmp Ceq with 0.0, no longer by structural
equality.)


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

Minor updates on ARM code generator.


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

Finished proof of chunktype_compat, which was incomplete.


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

Clight and C#minor.  Recognize __builtin_fabs and turn it into this operator.


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

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

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

- added __builtin_trap()
- generate .size and .type directives
- use natural alignment for variables


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

Algorithmic efficiency: in cparser/, precompute sizeof and alignof of composites.
Code cleanup: introduced Cutil.composite_info_{def,decl}


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

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

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

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

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

PrintCsyntax, PrintAsm: improve printing of float literals.


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

- 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

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

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

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

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

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

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

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

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

  #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

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

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

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

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

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