| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
| |
FP literals can have size 4 or 8 bytes, and it's incorrect to put a 4-byte
literal in a mergeable section of chunk size 8.
Fixes: #447
|
|
|
|
|
|
|
|
| |
This has been known to happen, e.g. when using Flocq 4.0.
If we don't stop the build at this point, a `ccomp` executable is built
that fails every time it is run.
Closes: #438
|
|
|
|
| |
Follow-up to 353669f8f
|
|
|
|
| |
Fixes: #441
|
|
|
|
| |
No longer triggered since commit df076edfe.
|
|
|
| |
Adapt w.r.t. coq/coq#16004.
|
| |
|
| |
|
|
|
|
|
| |
Handle constructors with 5, 6 and 7 arguments.
Handle lists.
|
| |
|
|
|
|
| |
Fixes: #435
|
|
|
|
|
|
|
|
|
|
| |
As suggested by Léo Gourdin in #437.
The previous expansion as a plain "j" instruction fails when the jump
offset is too large to be represented (issue #436).
Fixes: #436
Closes: #437
|
| |
|
|
|
|
| |
Fixes: #434
|
|
|
|
|
|
|
|
|
| |
CompCert doesn't maintain a frame pointer in X29. However, it must treat
X29 as callee-save, so that CompCert-generated code can be called from code
that uses X29 as frame pointer.
This commit makes X29 callee-save. In places where X29 was used as a
temporary, X15 or X14 is used instead.
|
|
|
|
|
|
|
|
| |
- Honor "noreturn" attributes and _Noreturn declarations on calls to
function pointers.
- Don't crash if a function type is an unknown typedef.
(This can happen with local typedefs.)
Instead, conservatively assume this function can return.
|
|
|
|
|
|
|
| |
Since we are sure that all files passed have a valid extension we can
use the OCaml function Filename.remove_extension and don't need to pass
the suffixes.
Bug 33218
|
|
|
|
|
|
|
| |
At some places the ".c" was hard coded as suffix for computing the
output filenames. This lead to problems if for example `-S`or `-c` is
used with preprocessed files.
Bug 33196
|
|
|
|
|
|
| |
- Emit the warning even for functions without parameters `int f() {...}`
- Show what the type is after prototyping
- Refactor this part of `elab_fundef` slightly
|
| |
|
|
|
|
| |
Entirely handled during elaboration. No impact on the verified part of CompCert.
|
|
|
|
|
| |
Before, in casts, `int (*)()` was parsed like `int (*)(void)`.
This caused expressions like `((int (*)()) &f)(42)` to be rejected.
Declarations were correctly parsed.
|
|
|
|
|
| |
The `pp_indication` optional argument that governs formatting boxes
in types was not propagated recursively, causing boxes to appear.
|
|
|
|
|
|
| |
Enum types should only be compatible with the underlying integer type,
not all integer types.
Bug 33212
|
|\
| |
| | |
Upgrade to Flocq 4.1.
|
| | |
|
| | |
|
| |
| |
| |
| | |
Otherwise, BinarySingleNaN.Bleb_correct cannot be proved.
|
| | |
|
|/ |
|
|
|
|
| |
`Kloop1` should have been `Kloop2`.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For RISC-V we need to return the canonical NaN value if the argument of
a float32->float64 or float64->float32 conversion is any NaN.
This is in line with 11.3 from the RISC-V manual, the description of
the conversion operations as well as what the spike ISA simulator and
qemu do.
Other platforms convert the NaN payload (by truncation or expansion)
in float32->float64 and float64->float32 conversions.
Fixes: #428
|
|
|
|
|
|
|
| |
If any are found, make sure that `-fstruct-passing` was given.
Previously, we used to check the fixed arguments (as part of a call to
`checkFunctionType`) but not the variable arguments.
|
|
|
|
|
|
|
|
|
|
| |
The ops `Omaxf` and `Ominf` have the same semantics as `minsd` and
`maxsd` instruction, i.e. if both arguments are equal the second
argument is returned as well as for NaN.
The operations are the used in SelectOp to implement the built-in
function `__builtin_fmax` and `__builtin_fmin`.
Bug 32640
|
|
|
|
|
|
| |
If both arguments are zero the second argument is returned independ from
their sign.
Bug 32640
|
| |
|
|
|
|
|
|
|
| |
coq/coq#15442 changes the way `Program` names things, to make it uniform w.r.t. the standard naming schema.
This commit removes dependencies on the names chosen by `Program`. Should be backwards compatible.
Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr>
|
| |
|
|
|
|
|
|
|
|
|
|
| |
As written previously, OCaml can evaluate `nodeOfVar g v1` and
`nodeOfVar g v2` in any order. Consequently, `v1` and `v2` can be
entered in the `varTable` hash table in different order. This can
result in different (but equally valid) register allocations.
It's better to enforce one evaluation order for the sake of
reproducible compilations when the OCaml version changes.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Add one more `Local Transparent Node` to ensure compatibility with Coq < 8.12
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This PR replaces the "PTree" data structure used in lib/Maps.v by the
canonical binary tries data structure proposed by A. W. Appel and
described in the paper "Efficient Extensional Binary Tries",
https://arxiv.org/abs/2110.05063
The new implementation is more memory-efficient and a bit faster,
resulting in reduced compilation times (-5% on typical C programs, up
to -10% on very large C functions).
It also enjoys the extensionality property (two tries mapping equal
keys to equal data are equal), which simplifies some proofs.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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".
|
|
|
|
|
|
|
|
|
|
|
|
| |
In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were
swapped:
- rldl is for [00001111] masks that clear on the left,
hence start with 1s and finish with 0s;
- rldr is for [11110000] masks that clear on the right,
hence start with 0s and finish with 1s.
In Asmgen.v, the case for masks of the form [00011111100] that can
generate a rldic instruction was incorrectly detected.
|
|
|
|
|
|
|
|
| |
CompCert does not support 128-bit integers, but the gcc and clang preprocessors do include support as part of its 'built-in'.
A common way of testing for 128-bit integer support is to check to see if `__SIZEOF_INT128__` is defined.
Eliminating this macro prevents software from believing that 128-bit integers are supported.
|