| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Introduce an error message for section attributes with non string
arguments,and another for multiple, ambiguous section attributes.
This is more consistent with the handling of other
attributes, like packed, than the old behavior of silently
ignoring them.
|
| |\ \
| | | |
| | | |
| | | | |
Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
|
| | | | |
|
| | |\| |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
The proof script for Events.excall_free_ok was incomplete
if Archi.ptr64 is unknown (as in the RISC-V case).
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
According to ISO C, `free(NULL)` is correct and does nothing.
This commit updates accordingly the formal semantics of the `free`
external function and the reference interpreter.
Closes: #334
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Currently we require the memory to be unchanged on readonly locations.
This is too strong. For example, current permissions could decrease
from readonly to none.
This commit weakens the ec_readonly condition to the strict minimum
needed to show the correctness of value analysis for const globals.
|
| | | | |
|
| |\ \ \
| | |_|/
| |/| |
| | | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
|
|\ \ \ \ |
|
| |\| | |
| | |/ /
| |/| |
| | | | |
mppa-work-upstream-merge
|
| | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Before it was "option typ". Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).
One benefit is that external functions get more precise types that
control better their return values. As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.
|
|/ / |
|
|\ \ |
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
|\ \ |
|
| |\|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Conflicts:
.gitignore
backend/Lineartyping.v
common/Values.v
configure
cparser/Machine.ml
cparser/Machine.mli
driver/Configuration.ml
driver/Frontend.ml
runtime/Makefile
test/c/Makefile
test/c/aes.c
test/compression/Makefile
test/regression/Makefile
test/regression/extasm.c
test/regression/floats-basics.c
test/regression/floats.c
Note : test/regression should be checked, didn't test it yet
|
| | | |
|
|\ \ \
| | | |
| | | |
| | | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
|
| |\ \ \
| | |/ /
| |/| /
| | |/ |
mppa-work-upstream-merge
|
| | |\
| | | |
| | | |
| | | | |
Support target architecture AArch64 (ARMv8 in 64-bit mode)
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
|
| | | | |
|
| | | | |
|
|/ / / |
|
|\| |
| | |
| | |
| | | |
mppa-work-upstream-merge
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
* Added semantic for byte swap builtins
The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics.
The semantics is given in terms of the decode/encode functions used for the memory model.
* Added bswap64 expansion to PowerPC 32 bits.
* Added bswap64 expansion for ARM.
|
| |/
| |
| |
| |
| | |
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
|
|\|
| |
| |
| | |
mppa-work-upstream-merge
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit adds mechanisms to
- recognize certain built-in and run-time functions by name and signature;
- associate semantics to these functions, as a partial function from
list of values to values;
- interpret external calls to these functions according to this semantics
(pure function from values to values, memory unchanged, no observable
events in the trace);
- external calls to unknown built-in and run-time functions remain
interpreted as generating observable events and possibly changing
memory, like before.
The description of the built-ins is split into a target-independent
part (in common/Builtins0.v) and a target-specific part (in
$ARCH/Builtins1.v).
Instruction selection uses the new mechanism in order to
- recognize some built-in functions and turn them into operations
of the target processor. Currently, this is done for
__builtin_sel and __builtin_fabs; more to come.
- remove the axioms about int64 helper functions from the standard
library. More precisely, the behavior of these functions is
still axiomatized, but now it is specified using the more general
machinery introduced in this commit, rather than ad-hoc axioms
in backend/SplitLongproof.
The only built-ins currently described are __builtin_fsqrt (for all platforms)
and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be
added later.
|
| |
| |
| |
| |
| | |
If the source language is determinate, it can take several steps
(not just one) before the "match_state" invariant is reinstated.
|
|\ \
| | |
| | |
| | | |
mppa-if-conversion
|
| |/
| |
| |
| |
| | |
If the source language is determinate, it can take several steps
(not just one) before the "match_state" invariant is reinstated.
|
| |
| |
| |
| |
| |
| | |
This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
`Val.select ob v1 v2 ty` is a conditional operation that chooses between
the values `v1` and `v2` depending on the comparison `ob : option bool`.
If `ob` is `None`, `Vundef` is returned.
If the selected value does not match type `ty`, `Vundef` is returned.
This operation will be used to model a "select" (or "conditional move")
operation at the CminorSel/RTL/LTL/Mach level.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size. These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.
This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.
|
| |
| |
| |
| |
| | |
Instead, use definitions and lemmas from the Coq standard library
(ZArith, Znumtheory).
|