| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| | |
|
|\| |
|
| | |
|
| |
| |
| |
| | |
This reverts commit 5ad25465f77c3009eaff7e9a124c254c1e9f33cd.
|
| | |
|
| | |
|
| | |
|
| | |
|
|/
|
|
| |
idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
|
|\
| |
| |
| |
| |
| | |
Conflicts:
.gitignore
runtime/include/stdbool.h
|
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
.gitignore
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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
|
| |
| |
| |
| |
| |
| | |
Fix various typos in diagnostic messages and unified wording and
capitalization.
Bug 23850
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* Outgoing stack slots are set to Vundef on return from a function call,
modeling the fact that the callee could write into those stack slots.
(CompCert-generated code does not do this, but code generated by other
compilers sometimes does.)
* Adapt Stackingproof to this new semantics. This requires tighter
reasoning on how Linear's locsets are related at call points and
at return points.
* Most of this reasoning was moved from Stackingproof to Lineartyping,
because it can be expressed purely in terms of the Linear semantics,
and tracked through the wt_state predicate.
* Factor out and into Conventions.v: the notion of callee-save
locations, the "agree_callee_save" predicate, and useful lemmas on
Locmap.setpair. Now the same "agree_callee_save" predicate is used
in Allocproof and in Stackingproof.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
|
| | |
|
| | |
|
| | |
|
|/ |
|
|
|
|
|
|
|
| |
This should avoid cluttering the assembler output with .ascii "\n"
lines if the annotation ends with a string and make for a better
readability.
Bug 23169
|
|
|
|
|
| |
Init_space has an argument of type Z and it can exceed the range of a 32-bit integer.
Reported by Frédéric Besson.
|
|
|
|
|
|
| |
It seems necessary that the mulitplication for the high part of
split registers is put into brackets.
Bug 23169
|
|
|
|
|
|
| |
This will soon be deprecated by Coq.
Manual merge of pull request #224 by vbgl. Closes: #224
|
| |
|
|
|
|
|
|
| |
Printing variable names with the default expression printer
results in newlines in the outputed error message.
Bug 23169
|
|
|
|
|
|
| |
The strings for json need quoting of special characters such as
\" and \\.
Bug 22438
|
|
|
|
|
|
| |
This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438
|
|
|
|
|
|
|
|
| |
Include the format specifier in error message when available in
order to make it easier to spot the broken ais parameter.
Futhermore introduce a new warning for unused ais parameters.
Bug 22464
|
| |
|
|
|
|
|
| |
Mention that it is a global memory cell.
Fix 22464
|
|
|
|
|
|
|
|
| |
The checks on the argument and format arguments are now performed
during C2C translation by calling the validate_ais_annotations
function and result in an error instead of a warning in the
backend to be more consistent with the rest of the builtin
functions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
|