| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For anonymous bit-fields in structs, carrier fields may
be introduced which are not initialized since no default
initializer are generated earlier. This cause the translation in
C2C to throw an error since too few initializers are available.
Example:
struct s2 {
int : 10;
int a;
int : 10;
char b;
int : 10;
short c;
int : 10;
} s2 = { 42, 'a', 43 };
To work around this issue we need to generate a default inializer
for every new member that does not have a translated member.
Based on P#80, with more efficient algorithms.
Bug 23362
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For each struct or union that contains bitfields,
we record the list of members after transformation,
where bit fields were replaced by carrier fields.
Right now we do not use this information but it will come handy
to fix a problem with struct initialization.
Also: clear the global hash tables on entry so that multiple runs
of the Bitfields transformation don't interfere with each other.
There probably was no interference before because identifiers are unique
enough, but this is fragile.
|
|
|
|
|
|
|
|
|
|
|
| |
Bit fields in unions were initialized like normal fields,
causing mismatch on the name of the field.
Also: added function Bitfields.carrier_field and refactored.
Patch by Bernhard Schommer.
Bug 23362
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
The "fix <number>" tactic is deprecated in Coq 8.8.0 and triggers warnings.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We were previously at 2.5.2. Quoting the NEWS from upstream:
Version 2.6.1:
- ensured compatibility from Coq 8.4 to 8.8
Version 2.6.0:
- ensured compatibility from Coq 8.4 to 8.7
- removed some hypotheses on some lemmas of Fcore_ulp
- added lemmas to Fprop_plus_error
- improved examples
Also: in preparation for Coq 8.8, silence warning "compatibility-notation"
when building Flocq, because this warning is on by default in 8.8,
and Flocq triggers it a lot.
|
|
|
|
| |
Forward declarations of enums are not allowed in C99, however it is possible to
have an empty enum declaration after the enum was defined.
|
|
|
|
|
|
| |
In the case of pointer subtraction both side can be pointers, for
example if the difference between two array cells is calculated,
so we need to check that both sides have complete types.
Bug 23312
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Adds a warning when a volatile struct is assigned to another
struct, that the volatile qualifier is ignored in this context.
Example:
```
volatile struct S s;
struct S t;
t = s; // did not warn before; now it warns
s = t; // did warn already
```
Bug 23489
|
|
|
|
|
|
|
|
|
|
|
|
| |
After calling enter_or_refine for a function identifier we need to keep
the combined attributes. Here is an example where it makes a difference:
```
_Noreturn void f(int x);
void f(int x) { }
```
Before this commit, the `_Noreturn` on the declaration is ignored when checking the definition.
Bug 23385
|
| |
|
|
|
|
|
|
| |
This part of PR#81 causes problems with long double static variables
in math.h. Revert to the old behavior of not including static
variables unless actually referenced.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(#81)
* Added check for redefinition of globals.
Since Cleanup may remove duplicated static functions or global
definitions we need to check for duplication during elaboration,
not just in C2C.
Bug 23410
* Do not eliminate unreferenced static variables with initializers
This way all initialized variables make it to the C2C pass,
where the initializers are checked for constant-ness.
Bug 23410
|
|
|
|
|
|
|
| |
Examples such as the following were accepted but are invalid ISO C:
char c[4] = 42;
struct S { int x, y; } = 42;
This commit rejects such initializations at top-level.
Bug 23372
|
|
|
|
|
|
|
|
| |
These macros can be defined to indicate that variable length
arrays, the _Complex type, atomics and threads are not supported.
Since the _Complex type is not supported, we also need
to undefine __STDC_IEC_559_COMPLEX__
Bug 23408
|
|
|
|
|
|
| |
It is allowed to define a composite within a bitfield size
expression using for example sizeof.
Bug 23360
|
|
|
|
|
|
| |
Substraction is only allowed for pointer - pointer,
pointer - arithmetic or arithmetic - arithmetic. This also leads
to a retyping error later.
Bug 23357
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Consider:
struct P { int x, y; }
struct S { struct P p; }
struct P p0 = { 1,2 };
struct S s1 = { .p = p0; .p.x = 3 };
ISO C99 and recent versions of Clang initialize s1.p.y to 2, i.e.
the initialization of s1.p.y to p0.y implied by ".p = p0" is kept,
even though the initialization of s1.p.x to p0.x is overwritten
by ".p.x = 3".
GCC, old versions of Clang, and previous versions of CompCert
initialize s1.p.y to the default value 0. I.e. the initialization
".p = p0" is forgotten, leaving default values for the fields of .p
before ".p.x = 3" takes effect.
Implementing the proper ISO C99 semantics in CompCert is difficult,
owing to a mismatch between the intended semantics and the C.init
representation of initializers.
This commit turns the delicate case of reinitialization above
(re-initializing a member of a composite that has already been
initialized as a whole) into a compile-time error.
We will then see if the delicate case occurs in practice and needs
further attention.
|
|
|
|
|
|
|
|
|
|
|
| |
The ISO C99 standard allows cast only if the type name involved
is either a void type or a scalar type.
For compatibility with GCC and Clang we used to support casting
a struct or union to exactly the same struct or union type.
That does not seem useful in practice and complicates conformance
testing. This commit gets rid of this exception to the C99 rule.
Bug 23310
|
|
|
|
|
| |
Instead of overwriting the initializer of the anonymous member we
should just keep it.
Bug 23353
|
| |
|
|
|
|
|
|
|
| |
Implicit Arguments is deprecated in Coq since 8.6 or so.
Some Implicit Arguments remained in Flocq but were recently changed to Arguments.
Apply the same change to our local copy of Flocq.
As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
|
|
|
|
|
|
|
| |
Sizeof and _Alignof are not allowed on bit-fields
Sizeof and _Alignof are not allowed to be applied to a expression
that designates a bit-field member.
Bug 23311
|
| |
|
|
|
| |
Unions containing multiple bit fields were transformed incorrectly.
|
|
|
|
|
|
|
| |
Arrays should decay to pointers except if they are used as operands of sizeof, _Alignof or as
operand of the unary &. The "comma" sequencing operator was missing a "decay" on the type of its second argument. All other operators "decay" their operands correctly.
Bug 23299
Bug 23311
|
|
|
|
|
|
| |
If an anonymous bit-field member is declared wrong, i.e. a wrong
type is used or a too large size is used the error message now
prints <anonymous> instead of an empty string.
Bug 23292
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Do not allow inline on main().
The C99 standard says that in a hosted environment inline shall
not appear in a declaration of main.
Bug 23274
* Added warning for _Noreturn on main().
The C11 standard does not allow any function specifier on the
main function.
Bug 23274
|
|
|
|
|
|
|
| |
This should avoid cluttering the assembler output with .ascii "\n"
lines if the annotation ends with a string and make for a better
readability.
Bug 23169
|
|
|
|
|
|
| |
It's OK to ignore *.o in any directory, but it's safer to ignore
"/ccomp" (ccomp in the top-level directory) than to ignore
"ccomp" (ccomp in any directory).
|
|
|
|
|
| |
Init_space has an argument of type Z and it can exceed the range of a 32-bit integer.
Reported by Frédéric Besson.
|
|
|
|
|
|
| |
It seems necessary that the mulitplication for the high part of
split registers is put into brackets.
Bug 23169
|
|
|
|
|
| |
The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3.
Fix 23199
|
|
|
|
|
|
| |
This will soon be deprecated by Coq.
Manual merge of pull request #224 by vbgl. Closes: #224
|
| |
|
|
|
|
|
| |
struct/union arguments to annotations should not be transformed at top level,
but the regular function calls contained within must be transformed recursively.
|
|
|
|
|
|
|
| |
In order to ensure that no transformation for arguments to
builtin annotations are used, the original unchanged arguments are
used.
Bug 23179
|
|
|
|
|
|
|
| |
This should help with parallel builds, which currently fail sometimes
owing to a lack of a dependency on pre_parser_aux.cmi.
Also: move documentation comments from the .ml to the .mli
|
|
|
|
|
|
|
|
|
|
|
|
| |
Make sure struct/union arguments to __builtin_annot and related
builtins are always passed by reference using the default passing mode,
regardless of the ABI for passing struct/unions to "real" functions.
This ensures portability of annotations across ABIs, and avoids mismatches
between the annotation text and the actual number of arguments
(when a struct/union argument is passed as N integer arguments).
A similar special case already existed for __builtin_va_arg.
|
|
|
|
|
|
| |
Printing variable names with the default expression printer
results in newlines in the outputed error message.
Bug 23169
|
|
|
|
|
|
| |
The strings for json need quoting of special characters such as
\" and \\.
Bug 22438
|
|
|
|
|
|
| |
x2 is the stack pointer of the riscV, both sp and x2 are supported
but to be safe use x2 in annotations.
Bug 23176
|
| |
|
|
|
|
|
|
| |
This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438
|
|
|
|
|
|
| |
It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and
'sp' for riscV.
Bug 23176.
|
|
|
|
|
| |
Registers should not contain the % prefix for ais annotations.
Bug 23176
|
|
|
|
|
|
|
|
| |
Include the format specifier in error message when available in
order to make it easier to spot the broken ais parameter.
Futhermore introduce a new warning for unused ais parameters.
Bug 22464
|