| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| | |
|
| |\
| |
| |
| | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
|
| | | |
|
| |/ |
|
| | |
|
| |\
| |
| |
| |
| |
| | |
Conflicts:
.gitignore
runtime/include/stdbool.h
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Follow-up to commit fc9bc643. The latest Menhir version compatible
with the current code base is actually 20181113.
|
| | | |
|
| | |
| |
| | |
The Coq backend of Menhir will soon enjoy a large refactoring, making it incompatible with the version of MenhirLib currently in CompCert. This commit adds a check in configure to make sure that the version of Menhir is not more modern than the current one (20181026).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
Expected results were obtained with GCC 5.4 and Clang 8.0
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
This file is created by Coq when running some tactics
|
| | |
| |
| | |
Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
|
| | |
| |
| |
| | |
No other changes are needed to support 8.9.0.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
ISO C2011 7.19 para 3 says "NULL, which expands to an implementation-defined null pointer constant"
ISO C2011 6.3.2.3 para 3 says "An integer constant expression with the value 0, or such an expression cast to type void *, is called a null pointer constant."
So, it seems NULL can be defined either as "0" or as "(void *) 0". However, the two definitions are not equivalent in the context of a call to a variadic or unprototyped function: passing 0 when the function expects a pointer value can go wrong if sizeof(int) != sizeof(void *).
This commit changes the definition of NULL to the safer one:
This is what GCC and Clang do in C mode; they use "#define NULL 0" for C++ only.
Fixes issue #265
|
| | |
| |
| |
| |
| | |
Sometimes a vararg function receives a NULL-terminated list of pointers.
This can fail if sizeof(NULL) < sizeof(void *), as this test illustrates.
|
| | |
| |
| |
| |
| |
| | |
As specified in ISO C99 section 7.16 and C11 section 7.18.
Fixes issue #266
|
| | |
| |
| |
| | |
Links to machine-specific modules were garbled during editing.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \
| | |
| | |
| | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |\ \ |
|
| | | | | |
|
| | |/ / |
|
