| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
| |
__builtin_offsetof(struct s, f) is an error if f is a bit-field.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field):
- the reference implementation, in Coq, from cfrontend/Ctypes.v
- the implementation used during elaboration, in OCaml, from cparser/Cutil.ml
The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used.
This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example:
```
struct __packed__(1) s { char c; short s; int i; };
assert (__builtin_offsetof(struct s, i) == 3);
assert (sizeof(struct s) = sizeof(char[sizeof(struct s)]));
```
The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs.
This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout.
Related changes:
* cparser/Cutil: add `packing_parameters` function to extract packing info from attributes
* cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout
* cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.)
* cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)).
* cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab
* cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/.
* test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.
|
|
|
|
|
| |
It is not allowed in C to have a parameter in a parameter list
without an identifier.
Bug 24283
|
|
|
|
|
|
| |
Since a non modifiable lvalue is an invalid asm output it should
be checked earlier, otherwise this leads to a retyping error
later.
Bug 24285
|
|
|
|
|
|
| |
Parameters also need to be checkd for unknown attributes, like
all other declarations.
Bug 24277
|
|
|
|
|
| |
The option -doptions was never document and no longer works.
Bug 19775
|
|
|
|
|
|
| |
Fix various typos in diagnostic messages and unified wording and
capitalization.
Bug 23850
|
|
|
|
|
|
| |
Since Pldi generates two instructions instr_size of Pldi should
return 2.
Bug 24218
|
| |
|
|
|
|
| |
better name for generated test cases.
|
|
|
|
|
|
|
| |
Additionally an open !Integers is needed for the open Integers in the
RISC-V Asmexpand, since Integers defines an Int64 module. This silences
the warning 44 triggered.
Bug 24090
|
|
|
|
| |
bug 24105, issue #243: expand correct version of ctzl/clzl builtin when long type is 64bit wide
|
| |
|
|
|
|
|
| |
This is a follow-up to commit 6e1a5ce.
Another `open! Floats` is needed.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
OCaml 4.07 introduces a Float submodule of the Stdlib
opened-by-default compilation unit. CompCert's Float compilation unit
also has a Float submodule. This triggers warning 44 when Floats is
opened. The workaround is just to silence the warning with `open! Floats`.
Closes: #241
|
| |
|
| |
|
|
|
| |
The `-iquote` option was passed to the GNU preprocessor as `-iquore`
|
|
|
|
|
| |
Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info.
Closes: #226.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Outgoing stack slots are set to Vundef on return from a function call,
modeling the fact that the callee could write into those stack slots.
(CompCert-generated code does not do this, but code generated by other
compilers sometimes does.)
* Adapt Stackingproof to this new semantics. This requires tighter
reasoning on how Linear's locsets are related at call points and
at return points.
* Most of this reasoning was moved from Stackingproof to Lineartyping,
because it can be expressed purely in terms of the Linear semantics,
and tracked through the wt_state predicate.
* Factor out and into Conventions.v: the notion of callee-save
locations, the "agree_callee_save" predicate, and useful lemmas on
Locmap.setpair. Now the same "agree_callee_save" predicate is used
in Allocproof and in Stackingproof.
|
| |
|
| |
|
|
|
|
| |
The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
|
| |
|
|
|
|
| |
Inspired by and adapted from pull request #235 by Benoît Viguier.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
Nonstatic inline functions can be expanded in several compilation units.
The static variables in question may differ between different expansions.
This is a manual merge and adaptation of pull request #P95 by @bschommer.
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before, we would pass just the `ctx_vararg` component of the context
to `elab_expr` as a Boolean argument.
For future extensions, we will need to pass more of the context to
`elab_expr`, so why not pass the whole context?
This is what this commit does. The `stmt_context` type is renamed
`elab_context` and its definition is moved earlier. The `ctx`
argument is passed as is from `elab_stmt` to `elab_expr`.
|
|
|
|
|
|
|
| |
The current check for redefinition is too strict, ruling out e.g.
```
typedef int t;
void f(void) { typedef char t; }
```
|
|
|
|
|
|
| |
These are extensions w.r.t. C99, not incompatible changes.
Nothing bad can happen if those C11 features are used, except making
the code incompatible with C99.
|
|
|
|
| |
Consistently with _Noreturn, anonymous structs, etc.
|
|
|
|
|
| |
It's not really necessary, and under Windows it's really ../../clightgen.exe,
which confuses make.
|
|
|
|
|
|
|
|
|
|
| |
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
|
|
|
|
|
| |
coq2html is now a standalone project (https://github.com/xavierleroy/coq2html)
packaged as coq-coq2html in OPAM-Coq.
|
|
|
|
| |
Also: add "parallel" entry to test/Makefile for parallel execution of tests.
|
|
|
| |
This is useful for the VST project and can be useful for others.
|
| |
|
|\ |
|
| | |
|
| | |
|