| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
This makes compilation runs more reproducible.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The struct member byte and bit offsets are now set based upon the new
function `struct_layout` from Ctypes.v, thus using the same code to
compute as used to generate the actual struct access.
The struct offset member information is addded using the types computed
after the translation in C2C. Therefore we need to store the new internal
names of the members as well as the composites and use them
when adding the offset information.
Fixes: #445
|
|
|
|
|
| |
The `struct_layout` function computes for each member, that is neither
padding nor zero-length, the same result as `field_offset`.
|
|
|
|
|
| |
Note that strings containing null characters (code 0) cannot be put in
a mergeable section, as this will confuse the linker's merging criterion.
|
|
|
|
|
|
|
|
|
|
|
|
| |
On platforms that support them (ELF, macOS), use mergeable sections
(like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals.
Works only if the LITERAL section is the default one. If the user
provided their own LITERAL section, all literals are put in it
regardless of their sizes.
Support for mergeable string sections is introduced in this commit too
but needs further changes in C2C.ml .
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
| |
|
| |
|