| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Before, the line number had to start with a nonzero digit. However,
the GCC 11 preprocessor was observed to produce `# 0 ...` directives.
Fixes: #398
|
| | | |
| | |
| | |
| | | |
E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Also: limit the max width of the page, to avoid very long lines.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
A bitfield assignment `x.b = f()` is expanded into a read-modify-write
on `x.carrier`. Wrong results can occur if `x.carrier` is read before
the call to `f()`, and `f` itself modifies a bitfield with the same
carrier `x.carrier`.
In this temporary fix, we play on the evaluation order implemented by
the SimplExpr pass of CompCert (left-to-right for side-effecting
subexpression) to make sure the read part of the read-modify-write
sequence occurs after the evaluation of the right-hand side.
More substantial fixes will be considered later.
Fixes: #395
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Not yet used for optimizations.
Actually, __builtin_expect is removed during C2C conversion, otherwise
the conversion to type "long" produces inefficient code on 64-bit platforms.
|
| | | |
| | |
| | |
| | | |
Not yet used for optimizations.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The following is correct but was causing a "wrong type for array initializer"
fatal error.
```
struct s { int n; int d[]; };
void f(void) { struct s x = {0}; }
```
Co-authored-by: Michael Schmidt <github@mschmidt.me>
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Variables without init do not generated any assembly code so no entry in
the json AST should be generated. They correspond to extern variables
without initializer that are defined in another compilation unit.
Bug 30112
|
| | | |
| | |
| | |
| | |
| | | |
Seems necessary for the standard headers of a recent version of XCode.
The actual definition in the standard headers is only for GNUC.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Volatile load and store are expanded later and also use the ld/std
instructions, therefore the same fixes that are applied as well for
them.
Bug 30983
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The offsets immediates used in the ld and std instructions must be a
multiple of the word size. This commit changes the two functions which
are used when generating load/stores in Asmgen, accessind and
transl_memory_access.
For accessind one only needs an additional check that the offset is a
multiple of the word size for the case that the high part of the offset
is zero, since otherwise the immediate is loaded into a register anyway.
The transl_memory_access function needs some slightly more complex
adoption. For all variants that do not construct the address in a
register before hand we must check that the offsets are multiples of the
word size and additionally if a symbol is used that the alignment of the
symbol is also a multiple of the word size. Therefore a new parameter is
introduced that allows checking the alignment.
In order to reduce the code duplication for the proofs these two
functions get an additional parameter in order to indicate wether the
offset needs to be a multiple of the word size or not.
Bug 30983
|
| | | |
| | |
| | |
| | | |
Follow-up to bb5dab848
|
| | | |
| | |
| | |
| | |
| | | |
The `-version-file` option was removed in commit 600803cae, but remained
in the option summary, as reported in #386.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This avoids a nasty conflict with Ltac2 notations as reported in #392.
The old `$` notation in scope `string_scope` was not used yet, AFAIK.
The new submodule and the new scope are the right places to add future
notations to facilitate working with the output of clightgen.
Fixes: #392
|
| | | | |
|
| | | |
| | |
| | |
| | | |
This is required to have List.repeat in the standard library (next commit).
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
When desugaring a bitfield, allow any integral type that is 32 bits
or smaller. Previously this was checking the rank of the type rather
than the size.
This rank check caused issues with standard headers that
declare `uint32_t` to be an `unsigned long` rather than an
`unsigned int`. Here, any bitfields declared as `uint32_t` were
failing to compile even though they are still actually 32 bits.
Co-authored-by: Amos Robinson <amos@gh.st>
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Use pipeline notation `|>` for legibility and better GC behavior
(in bytecode at least).
- Introduce auxiliary functions.
- Remove useless function parameters.
- Fix the timing of the "Emulations" pass
(because of an extra parameter, what was timed took zero time).
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
After Menhir version 20210310, the `Fail_pr` constructor of the
`parse_result` type becomes `Fail_pr_full` with two extra arguments.
This PR enables CompCert to handle both versions of the `parse_result`
type in MenhirLib.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters.
There was one place in CompCert where one of these automatically-generated names was used.
This commit avoids using this name.
|
| |\ \ \ |
|
| | | | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
|
| | | | | | |
|
| | |/ / / |
|
| | | | | |
|
| | |\ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
