| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |\
| |
| |
| | |
Mostly changes in PTree
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The previous code for elaborating character constants has a small bug:
the value of a wide character constant consisting of several characters
was normalized to type `int`, while, statically, it has type `wchar_t`.
If `wchar_t` is `unsigned short`, for example, the constant `L'ab'`
would elaborate to 6357090, which is not of type `unsigned short`.
This commit fixes the bug by normalizing wide character constants to type
`wchar_t`, regardless of how many characters they contain.
The previous code was odd in another respect: leading `\0` characters
in multi-character constants were ignored. Hence, `'\0bcde'` was accepted
while `'abcde'` caused a warning.
This commit implements a more predictable behavior: the number of characters
in a character literal is limited a priori to
sizeof(type of result) / sizeof(type of each character)
So, for non-wide character constants we can typically have up to 4
characters (sizeof(int) / sizeof(char)), while for wide character
constants we can only have one character.
In effect, multiple-character wide character literals are not supported.
This is allowed by the ISO C99 standard and seems consistent with GCC
and Clang.
Finally, a multi-character constant with too many characters was
reported either as an error (if the computation overflowed the 64-bit
accumulator) or as a warning (otherwise). Here, we make this an error
in all cases.
GCC and Clang only produce warnings, and truncate the value of the
character constant, but an error feels safer.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Earlier CompCert versions would warn if a bit field of width N and
type enum E was too small for the values of the enumeration: whether
the field is interpreted as a N-bit signed integer or a N-bit unsigned
integer, some values of the enumeration are not representable.
This warning was performed in the Bitfields emulation pass, which went
away during the reimplementation of bit fields within the verified
part of CompCert.
In this commit, we resurrect the warning and perform it during the Elab pass.
In passing, some of the code that elaborates bit fields was moved to a
separate function "check_bitfield".
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When a union is initialized with an initializer without designator the
first named member should be initialized. This commit skips members
without names during the elaboration of union initializers.
Note that anonymous members (unnamed members of struct or union type)
should not be skipped, and are not skipped since elaboration give names
to these members.
Bug 31982
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
E.g. `struct { int; int x; };`. The `int;` declaration provides no name,
is not a bit field, and is not a C11 anonymous struct/union member.
Such declarations are not allowed by the C99 grammar, even though GCC,
Clang and CompCert tolerate them. The C11 grammar allows these
declarations but the standard text gives them no meaning.
CompCert used to warn about such declarations, yet include them in the
struct or union as unnamed members, similar to an unnamed bit field.
This is incorrect and inconsistent with what GCC and Clang do.
With this commit, CompCert still warns, then ignores the declaration
and does not create an unnamed member. This is consistent with GCC
and Clang.
Fixes: #411
|
| | |
| |
| |
| |
| |
| | |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When desugaring a bitfield, allow any integral type that is 32 bits
or smaller. Previously this was checking the rank of the type rather
than the size.
This rank check caused issues with standard headers that
declare `uint32_t` to be an `unsigned long` rather than an
`unsigned int`. Here, any bitfields declared as `uint32_t` were
failing to compile even though they are still actually 32 bits.
Co-authored-by: Amos Robinson <amos@gh.st>
|
| | |
| |
| |
| | |
cfrontend/C2C.ml
|
| |\|
| |
| |
| |
| |
| |
| |
| |
| | |
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
|
| | |
| |
| |
| |
| |
| |
| | |
Follow-up to 35e2b11db.
Put the warning "pragmas are ignored inside functions" inside the Unnamed
category, so that it is displayed by default and cannot be disabled.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Pragmas can occur either outside external declarations, at the top level
of a compilation unit, or within a compound statement, inside a function
definition.
The parse tree in cparse/C.mli cannot represent pragmas occuring within
a compound statement.
In this case, the elaborator used to silently move the pragma to top
level, just before the function definition where the pragma occurs.
It looks safer to just ignore pragmas occurring inside a function
definition, and emit a specific warning.
|
| |\| |
|
| | |
| |
| |
| |
| | |
Also: improve check for ptr - integer.
(Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)
|
| | | |
|
| | |
| |
| |
| | |
We check that this builtin function is only called from within a variadic
function and has the correct number of arguments.
|
| | | |
|
| | |
| |
| |
| |
| | |
Returns 1 if the argument is a constant expression, 0 otherwise.
Closes: #366
|
| | |
| |
| |
| |
| |
| | |
We check in the initial environment if a function is already defined to
avoid redefinition of functions that are part of the builtin
environment.
|
| | |
| |
| |
| |
| |
| |
| | |
The function String.uppercase was deprecated and the replacement
function String.upercase_ascii was only available from OCaml 4.03.0.
Since the minimal OCaml version is now 4.05.0 we can use the function
String.upercase_ascii.
|
| |\| |
|
| | |
| |
| | |
In case of redefinition of a typedef name with a different type.
|
| | |
| |
| |
| | |
See ISO C2011 standard, section 6.4.4.4 para 11.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
"open!" is the form used in the examples in the OCaml manual.
Based on a quick poll it seems to be the preferred form of the OCaml
core dev team.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
| |
|
|
|
|
|
|
|
| |
Previously, using an unknown builtin function was treated like any
other call to an undeclared function: a warning was emitted, and
an error occurred at link-time.
With this commit, using an unknown builtin function is an error,
like in Clang.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Extend check for incomplete type.
Extended the check to also include a check for variables with
incomplete object type that are not arrays, that have an
initializer. Furthermore the warning includes the type and variable
name.
* Warning for incomplete type in compound literals.
Incomplete types are not allowed for compound literals, except for
array types.
* Extend type printing function.
The type of a typedeof of an anonymous type should not be printed.
Furthermore added '<anonymous>' to the printing of anonymous types.
* Unify incomplete type errors message.
The incomplete type error messages should all look the same including
name of the variable, parameter, etc. and then the incomplete type.
|
| |
|
|
|
|
| |
In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier).
Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
|
| |
|
|
|
| |
It is type-checked like a conditional expression then translated to
a call to the known builtin function.
|
| |
|
|
|
|
|
|
|
| |
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
What's new:
1. A rewrite of the Coq interpreter of Menhir automaton, with
dependent types removing the need for runtime checks for the
well-formedness of the LR stack. This seem to cause some speedup on
the parsing time (~10% for lexing + parsing).
2. Thanks to 1., it is now possible to avoid the use of int31 for
comparing symbols: Since this is only used for validation,
positives are enough.
3. Speedup of Validation: on my machine, the time needed for compiling
Parser.v goes from about 2 minutes to about 1 minute. This seem to
be related to a performance bug in the completeness validator and
to the use of positive instead of int31.
3. Menhir now generates a dedicated inductive type for
(semantic-value-carrying) tokens (in addition to the already
existing inductive type for (non-semantic-value-carrying)
terminals. The end result is that the OCaml support code for the
parser no longer contain calls to Obj.magic. The bad side of this
change is that the formal specification of the parser is perhaps
harder to read.
4. The parser and its library are now free of axioms (I used to use
axiom K and proof irrelevance for easing proofs involving dependent
types).
5. Use of a dedicated custom negative coinductive type for the input
stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
positive coinductive type, which are now deprecated by Coq.
6. The fuel of the parser is now specified using its logarithm instead
of its actual value. This makes it possible to give large fuel
values instead of using the `let rec fuel = S fuel` hack.
7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
The corresponding changes in Menhir have been released as part of
version 20190626. The `MenhirLib` directory is identical to the
content of the `src` directory of the corresponding `coq-menhirlib`
opam package except that:
- In order to try to make CompCert compatible with several Menhir
versions without updates, we do not check the version of menhir
is compatible with the version of coq-menhirlib. Hence the
`Version.v` file is not present in CompCert's copy.
- Build-system related files have been removed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The new diagnostics is triggered if a conditional is used that
may not be transformed into linear code by the later by the
if conversion.
The new diagnostic is emitted if a conditional may contain an
unsafe expression or is contained within another conditional,
logical and or logical or expression. An expression is unsafe if
it contains a call, changes memory or if its evaluation leads to
undefined behavior, for example division and modulo.
Also fixes a small typo in a comment in Cutil.
|
| |
|
|
| |
There should only be one unnamed parameter of type void in the
parameter list.
|
| |
|
|
|
|
| |
This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
|
| |
|
|
|
|
| |
The arguments that are passed to an unprototyped function must
also be checked to be valid types passed to a function, i.e. they
must be complete types after argument conversion.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Since a definition/declaration is completed with after the
separator to the next init group member it is also possible to
use it for example in the next init group member:
char s[]="miaou", buf[sizeof s];
In order to ensure that this works the declarations are added to
the environment directly during the elaboration of the init member
group instead of later.
|
| |
|
|
|
|
|
|
|
| |
Pass the environment to all expr eval functions since
the functions themselve may be called recursively and modify
the environment.
The other change introduces new scopes that are strict
subsets of their surrounding scopes for if, switch, while,
do and for statement, as prescribed by ISO C standards.
|
| |
|
|
|
|
| |
The previous check was incomplete for integer literals in base 10.
Bug 26119
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Consider:
```
struct s { ... } __attribute((aligned(N)));
struct t { ... }
__attribute((aligned(N))) struct t x;
```
In the first case, the aligned attribute should be attached to struct s, so that further references to struct s are aligned.
In the second case, the aligned attribute should be attached to the variable x, because if we attach it to struct t, it will be ignored and cause a warning.
This commit changes the attachment rule so that it treats both cases right.
Extend regression test for "aligned" attribute accordingly, by testing
aligned attribute applied to a name of struct type.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds a check to reject type definitions such as
```
typedef __attribute((section "foo")) int fooint;
```
GCC and Clang also reject this as an error.
Without the check, the behavior is somewhat surprising:
```
fooint x; // placed in section "foo"
fooint * x; // placed in default section, attribute "foo" is ignored
```
Note that the following must be accepted:
```
typedef struct { ... } __attribute((packed)) t;
```
The "packed" attribute is correctly attached to the struct type and should not be checked. This is achieved by using `attribute_of_type_no_expand` to get the attributes of the typedef-ed type, excluding the attributes carried by a struct/union or another typedef.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a second step towards mimicking GCC/Clang's handling of attributes.
This commit introduces a distinction between
- Object-related attributes, such as "section", which apply to the object (function, variable) being defined;
- Name-related attributes, such as "aligned", which apply to the name (object, struct/union member, struct/union/enum tag) being defined.
In particular, "aligned" is now attached to "struct" and "union" definitions, while it used to be "floated up" before.
The C11 _Alignas modifier is treated like an object-related attribute, so that
```
struct s { ... };
_Alignas(64) struct s x;
```
correctly associates the alignment with "x" and not with "struct s", where it would be ignored because it was not part of the original definition of s.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
During elaboration of type declarators, non-type-related attributes such as "aligned" or "section" are "floated up" so that they apply to the thing being declared. For example, consider:
```
__attribute((aligned(16))) int * p;
```
The attribute is first attached to type `int`, then floated up to type `int *`, so that it finally applies to `p`, giving a 16-aligned pointer to int, and not a naturally-aligned pointer to 16-aligned int.
What happens when the non-type-related attribute comes from a typedef?
```
typedef __attribute((aligned(16))) int i16;
i16 * p;
```
CompCert used to expand the typedef then float up the attribute, resulting in `p` being a 16-aligned pointer to int.
GCC and Clang produce a naturally-aligned pointer, so they do not expand the typedef before floating.
The old CompCert behavior is somewhat surprising, and potentially less useful than the GCC/Clang behavior.
This commit changes the floating up of non-type-related attributes so that typedefs and struct/union/enum definitions are not expanded when determining which attributes to float up. This is a first step towards mimicking the GCC/Clang behavior.
|
| |
|
|
|
|
| |
Catch the exception from a non constant argument of a packed
attribute and print an error.
Bug 24748
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* bug 24268: avoid assertion after reporting error for invalid call to builtin_debug
* bug 24268, remove duplicated warning tag in lexer messages
* bug 24268, fix spelling in array element designator message
* bug 24268, unify 'consider adding option ...' messages
* bug 24268, add spacing for icbi operands
* bug 24268, uniform use of Ignored_attributes class for identical warnings
* bug 24268, unify message for 'assignment to const type' to error from error/fatal error
* bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
|
