| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
|
| |
|
|
|
|
|
|
| |
Catch the exception from a non constant argument of a packed
attribute and print an error.
Bug 24748
|
|
|
|
|
| |
Otherwise an isel is generated if no isel is needed at all.
Bug 24516
|
|
|
|
|
|
| |
If the isel instruction is missing, it can be emulated just like we do
in the 32-bit case (__builtin_isel).
Follow-up to commit 51d32b92.
Bug 24516
|
|
|
|
|
| |
New builtin isel variants to support conditional moves for 64bit integers and _Bool values.
Bug 24516
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
This change avoids relying on generated names, making the proof script compatible with ongoing evolutions of the `zify` tactic.
A similar cleanup was already performed in Flocq's master sources.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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"
|
| |
|
|
|
|
|
| |
It's not out yet, but based on the state of the v8.8 branch of Coq,
it is very likely to be compatible with CompCert.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Generate a nop instruction after ais annotations.
In order to prevent the merging of ais annotations with following
Labels a nop instruction is inserted, but only if the annotation
is followed immediately by a label.
The insertion of nop instructions is performed during the
expansion of builtin and pseudo assembler instructions and is
processor independent, by inserting a __builtin_nop built-in.
* Add Pnop instruction to ARM, RISC-V, and x86
ARM as well as RISC-V don't have nop instructions that can
be easily encoded by for example add with zero instructions.
For x86 we used to use `mov X0, X0` for nop but this may
not be as efficient as the true nop instruction.
* Implement __builtin_nop on all supported target architectures.
This builtin is not yet made available on the C side for all architectures.
Bug 24067
|
|
|
|
|
|
| |
Since the following offsetof cannot handle bit-fields we should
stop earlier.
Bug 24480
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Refactor common code of alignas.
Instead of working on attributes the function now works directly
on the type since the check always performed an extraction of
attributes from a type.
Bug 23393
* Attach _Alignas to the name.
Bug 23393
* Attach "aligned" attributes to names
So that __attribute((aligned(N))) remains consistent with _Alignas(N).
gcc and clang apply "aligned" attributes to names, with a special case
for typedefs:
typedef __attribute((aligned(16))) int int_al_16;
int_al_16 * p;
__attribute((aligned(16))) int * q;
For gcc, p is naturally-aligned pointer to 16-aligned int and
q is 16-aligned pointer to naturally-aligned int.
For CompCert with this commit, both p and q are 16-aligned pointers
to naturally-aligned int.
* Resurrect the alignment test involving typedef
The test was removed because it involved an _Alignas in a typedef,
which is no longer supported. However the same effect can be achieved
with an "aligned" attribute, which is still supported in typedef.
|
| |
|
| |
|
|\ |
|
| | |
|
|/ |
|
|
|
|
|
|
| |
Instead of performing the check only for parameters of function
definitions also perform it for function declarations.
Bug 23393
|
|
|
|
|
|
|
| |
The new diagnostic triggers if an `_Alignas` or an `aligned` attribute
or a `packed` attribute requests an alignment smaller than the natural alignment.
Bug 23389
|
| |
|
|\
| |
| | |
Improve behavior of configure script in case of configuration errors
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The full "usage" text is so long that the actual error message scrolls off
the screen.
With this commit, instead, a short (3-line) error message is printed,
with a suggestion to do `./configure -help`.
The whole "usage" text is printed by `./configure -help`.
Also: better error message for unknown options (arguments starting with `-`).
|
| |
| |
| |
| |
| |
| |
| | |
So that if an error occurs during configuration, there is no
Makefile.config file and "make" will fail.
Closes: #244
|
| | |
|
| |
| |
| |
| |
| | |
Follow-up to f6f537d. "list" scope must be opened to counterbalance
opening of "string" scope.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is required for compatibility with
https://github.com/coq/coq/pull/8064, where prim token notations no longer
follow `Require`, but instead follow `Import`.
Closes #246
Closes #250
|
|/ |
|
|
|
|
|
|
|
| |
For consistency with other generated .v files, and because it protects
against editing the generated file, see Github issue #248.
Closes: #248
|
|
|
|
|
|
| |
- Make it possible to skip tests on some platforms
- Make it possible to expect a failure (typically: of the reference interpreter)
- Stop on error
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
The C11 standard disallows the usage of _Alignas for:
- Bit-field members of struct or union types
- Typedefs
- Function Defintions
- Parameters of functions
It is still allowed to use the gcc attribute for these constructs.
Bug 23391
|
|
|
|
|
|
| |
The check tests whether the standard _Alignas is contained within
a given attribute list.
Bug 23391
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Since commit 5963ac4, "aligned" attributes and _Alignas qualifiers
are represented differently, causing them to be treated differently
by the previous implementation of Cutil.attr_array_applicable.
This is incorrect and inconsistent with what happens during elaboration
of array types in Elab.
This PR reimplements attr_array_applicable in terms of class_of_attribute.
Just like during elaboration, attributes of the Attr_type class
are applied to the type of array elements, other attributes stay
attached to the array type.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We used to recognize attribute(("aligned"(N))) and map it to _Alignas(N)
during elaboration.
However, we want to restrict the places where _Alignas can occur, as
standardized in ISO C11, while leaving more freedom for the placement
of the "aligned" attribute.
As a first step in this direction, this commit keeps the "aligned"
attribute unchanged in the AST, and distinct from _Alignas attributes.
Both attributes are honored when it comes to determining the actual
alignment of a type.
|
| |
|
|
|
|
| |
type, bug 23377
|
| |
|
| |
|
|
|
|
|
|
| |
Instead of just passing -u to the linker also pass the value of
the option to the linker.
Bug 24316
|
|
|
|
|
|
| |
Restrict is only allowed for pointers whose referenced type is an
object type or incomplete type, but not a function type.
Bug 23397
|
|
|
|
|
| |
Follow-up to b9a6a50. clang is not happy with COMPCERT_MODEL=32sse2
("bad suffix on integer"), so use MODEL_32sse2 and ARCH_x86 instead.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Add diagnostic for type qualified arrays that occur in the wrong place
Arrays with type qualifiers (e.g. int t[const 5]) are only allowed as
function parameters and for them
only the outermost array type derivation.
Bug 23400
* Keep attributes from array for argument conversion
Type qualifiers of arrays in function parameters are just syntactic sugar
to allow adding them to the resulting pointer type. Hence, when a
qualified array type such as `int t[const 5]` decays into a pointer type
during argument conversion, the pointer type should be qualified, e.g. `int * const t`.
|
|
|
|
|
|
| |
Tentative static definitions with incomplete type are not allowed
in C99. However most popular compilers support them and warn
about them.
Bug 23377
|