| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
| |
The Elab pass checks that the argument of 'case' is a compile-time constant
expression. This commit records the value of this expression in the
C.Scase AST generated by Elab, so that it can be used for further
diagnostics, i.e. checking (in Elab) for duplicate cases.
Note that C2C ignores the recorded value and recomputes the value of
the expression using Ceval.integer_expr. This is intentional:
Ceval.integer_expr is more trustworthy, as it is formally verified
against the CompCert C semantics.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously, CompCert would just ignore the `auto` keyword, thus accepting
incorrect top-level definitions such as
```
auto int x;
auto void f(auto int x) { }
```
This commit introduces `auto` as a proper storage class
(Storage_auto constructor in the C AST).
It adds diagnostics for misuses of `auto`, often patterned after the
existing diagnostics for misuses of `register`.
Some error messages were corrected ("storage-class" -> "storage class")
or made closer to those of clang.
Finally, in the generated C AST and in C typing environments,
block-scoped variables without an explicit storage class are recorded
as Storage_auto instead of Storage_default. This is semantically correct
(block-scoped variables default to `auto` behavior) and will help us
distinguishing block-scoped variables from file-scoped variables
in later developments.
|
|
|
|
|
| |
This time with the correct place for setting the destination files.
Bug 20521
|
|
|
|
| |
Before, we were doing C90, there was no official syntax for such attributes, and we used ours. With C99 we can use "ty [ attributes N ]" to print "array with attributes of N elements of type ty".
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The treatment of attributes in the current CompCert is often surprising. For example,
attribute(xxx) char * x;
is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char".
CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e.
const char * x;
is really "x is a pointer to a const char", not "x is a const pointer to char".
This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above,
attribute(xxx) char * x; // "attribute(xxx)" applies to "x"
const char * x; // "const" applies to "char"
This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
|
|
|
|
|
|
| |
This avoids introducing line breaks during printing of function
types.
Bug 18004
|
| |
|
|
|
|
|
|
| |
Instead of creating separate annotations for the local variables
we call the Debug.add_lvar_scope and we construct a mapping from
function id + scope id to scope information.
|
| |
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
Elab: Handle C99 designated initializers.
C2C, Initializers: more precise intermediate AST for initializers.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- C function types and Cminor signatures annotated by calling conventions.
esp. vararg / not vararg
- Cshmgen: generate correct code for function call where there are
more arguments than listed in the function prototype. This is
still undefined behavior according to the formal semantics,
but correct code is generated.
- C2C, */PrintAsm.ml: remove "printf$iif" hack.
- powerpc/, checklink/: don't generate stubs for variadic functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
cparser: add primitive support for enum types.
bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
and __alignof__(ty), __alignof__(expr) from GCC.
- Resurrected __builtin_memcpy_aligned, useful for files generated
by Scade KCG 6.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
cparser: added experimental emulation of packed structs (PackedStruct.ml)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 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@1272 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|