| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
| |
CompCert currently uses `Instance` in so-called "refine" mode, where
Coq drops automatically in proof mode if some members of the instance
are missing.
This mode is soon going to be turned off by default, see
https://github.com/coq/coq/pull/9270.
In order to make CompCert robust against this change, this commit
replaces those occurrences of `Instance` that use "refine" mode
with `Program Instance`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As written in the comment, ZF should be set if the two floats are
equal or unordered. The "or unordered" case was missing in the
original modeling of FP comparisons.
- Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions.
- Update the proofs in Asmgenproof1 accordingly.
No change required to the code generated for FP comparisons: this code
already anticipated the "or unordered" case.
Problem reported by Alix Trieu.
|
|
|
|
|
|
|
| |
"compare" returns the 4 possible results w/ type "option comparison".
"ordered" returns a Boolean.
These functions will be used soon in the x86 port.
|
|
|
|
|
|
|
|
| |
Instead of relying testing that the size of pointers is 64bit the
size of registers should be tested. Also it should be a fatal
error to reverse a long long on an architecture that does not
support reverse 64bit read/writes.
Bug 24982
|
| |
|
| |
|
|
|
|
|
|
| |
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
|