| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
|
|
|
|
|
|
| |
The arguments that are passed to an unprototyped function must
also be checked to be valid types passed to a function, i.e. they
must be complete types after argument conversion.
|
|
|
|
|
| |
No `Osel` operation for this port, so `SelectOp.select` always
returns None.
|
|
|
|
|
| |
The operation comples down to conditional moves.
Both integer and floating-point conditional moves are supported.
|
|
|
|
| |
The operation compiles down to conditional moves.
|
|
|
|
|
| |
On non-EREF processors it expands to instructions that destroy GPR0.
Reflect this in the Asm semantics for Pisel.
|
|
|
|
|
| |
This operation compiles down to an `isel` instruction (conditional move).
The semantics is given by `Val.select`.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
`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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This will be useful to implement a "select" (conditional move) operation later.
- Introduce `Asmgen.loadimm64_notemp` to load a 64-bit integer
constant into a register without going through memory and without
needing a temporary register.
- Use `Asmgen.loadimm64_notemp` instead of `Asmgen.loadimm64` in the
compilation of conditions, so that GPR12 is no longer needed as a
temporary.
- Share code and proofs common to the two `Asmgen.loadimm64_` functions
as the `Asmgen.loadimm64_32s` function.
|
|
|
|
|
|
|
|
| |
Following the gnu Makefile Conventions the variable $(DESTDIR)
should be prepended to all installation commands. This allows
staged installs.
|
|
|
|
|
|
|
|
|
|
|
|
| |
Since a definition/declaration is completed with after the
separator to the next init group member it is also possible to
use it for example in the next init group member:
char s[]="miaou", buf[sizeof s];
In order to ensure that this works the declarations are added to
the environment directly during the elaboration of the init member
group instead of later.
|
|
|
|
|
|
|
|
|
|
| |
The option -fcommon controls whether uninitialized global
variables are placed in the COMMON section. If the option is given
in the negated form, -fno-common, variables are not placed in the
COMMON section. They are placed in the same sections as gcc does.
If the variables are not placed in the COMMON section merging of
tentative definitions is inhibited and multiple definitions lead
to a linker error, as it does for gcc.
|
|
|
|
|
| |
The AbsInt build number no longer contains "release", so it must
be printed additionally.
|
|
|
|
|
|
| |
`_Complex` and `_Imaginary` are reserved keywords. Since CompCert does
not support these types they could be used as identifiers. However
the standard requires to reject this.
|
|
|
|
|
|
|
|
|
| |
Pass the environment to all expr eval functions since
the functions themselve may be called recursively and modify
the environment.
The other change introduces new scopes that are strict
subsets of their surrounding scopes for if, switch, while,
do and for statement, as prescribed by ISO C standards.
|
|
|
|
|
| |
Since the error formatter is not automatically flushed at program
exit we need to ensure that it is flushed at exit.
|
|
|
|
|
|
|
|
|
| |
* Move the expansion of response files to module Commandline,
during the initialization of `Commandline.argv`.
This way we're sure it's done exactly once.
* Make `Commandline.argv` a `string array` instead of a `string array ref`.
We no longer need to update it after initialization!
* Improve reporting of errors during expansion of response files.
|
|
|
|
|
|
| |
Add a check for alignment on command-line switches `-falign-*`.
The check is similar to the one for the alignment attribute and
ensures that only powers of two can be specified.
|
|
|
|
|
|
| |
The previous implementation used to build the full powers-of-two decomposition
of the number. The present implementation recognizes powers of two directly,
then takes the log2.
|
|
|
|
|
|
|
|
| |
The `field_simplify` tactics will be improved soon (https://github.com/coq/coq/pull/9854).
Flocq was made compatible with this improvement (https://gitlab.inria.fr/flocq/flocq/commit/0752761a6a344d62f6bc728eac442ebb4ba655ac).
This commit updates CompCert's copy of Flocq accordingly.
|
|
|
|
|
| |
To match the new module names from version 3 of Flocq.
Plus, it's shorter.
|
|
|
|
|
|
|
|
|
|
| |
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).
|
|
|
|
|
|
|
| |
Use Z.to_nat theorems from the standard Coq library in preference to
our theorems in lib/Coqlib.v.
Simplify lib/Coqlib.v accordingly.
|
|\
| |
| |
| | |
Merge of branch dwarf-ranges
|
| |
| |
| |
| |
| |
| |
| | |
Instead of printing an the start label and adding the offset by
computing the difference of the range label and the start label
use the range label directly.
Bug 26234
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Functions that are removed from the compilation unit, for example
inline functions without extern, should not produce debug
information.
This commit reuses the mechanism used for variables in order to
track additionally the printed functions. Therefore the printed
variable versions are exchanged for a printed symbol version.
Bug 26234
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The fist changes changes the offset for range entries to used labels
instead of integer constants, leaving the computation to the
assembler.
The second part of the change the address changes the way ranges
entries of scopes are printed. They need to be relative to the start
address of the code in the section they are included.
Bug 26234
|
| |
| |
| |
| |
| |
| |
| | |
In order to avoid adding ranges to the wrong scopes due to
inlining they are numbered consecutively for the whole compilation
unit.
Bug 26234
|
| |
| |
| |
| |
| |
| | |
As noted in the DWARF 3 specification empty ranges have no effect
and can be left out.
Bug 26234
|
|/
|
|
|
|
| |
Ranges for non-contiguous address ranges are already part of dwarf
version 3.
Bug 26234
|
| |
|
|
|
| |
SEL_SWITH_INT -> SEL_SWITCH_INT
|
|
|
|
| |
These were committed by mistake.
|
|
|
|
|
|
|
|
| |
Rumor has it that this module is scheduled for removal.
This is based on pull request #286, with a different implementation.
Closes: #286
|
|
|
|
| |
In the `Sswitch` case, the original expression was used instead of the result of `norm_expr`.
|
|
|
|
|
| |
A grep through Coq's source files show that it uses more cache files
than just .lia.cache. Ignore them all.
|
|
|
|
|
|
|
|
|
|
|
|
| |
Main changes to CompCert outside of Flocq are as follows:
- Minimal supported version of Coq is now 8.7, due to Flocq requirements.
- Most modifications are due to Z2R being dropped in favor of IZR and to
the way Flocq now handles NaNs.
- CompCert now correctly handles NaNs for the Risc-V architecture
(hopefully).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As suggested in #282, it can be useful to #ifdef code depending on
specific versions of CompCert.
Assuming a version number of the form MM.mm ,
the following macros are predefined:
__COMPCERT_MAJOR__=MM (the major version number)
__COMPCERT_MINOR__=mm (the minor version number)
__COMPCERT_VERSION__=MMmm (two decimal digits for the minor, e.g. 305 for version 3.5)
We also define __COMPCERT_BUILDNR__ if the build number is not empty in file ./VERSION.
Closes: #282
|
|
|
|
|
|
|
|
|
|
|
| |
As reported in #281, the Menhir packages in Fedora 29 and perhaps in
other distributions can cause `menhir --suggest-menhirLib` to fail
and return an empty path.
This commit detects this situation and aborts configurations.
Also, it hardens the generated Makefile against spaces and special
characters in the path returned by `menhir --suggest-menhirLib`.
|
|
|
|
|
|
|
| |
`external_call_mem_extends` returns a conjunction of 4 properties,
but the destruct pattern was 5 level deep.
(Reported by Jeremie Koenig in pull request #278.)
|
|
|
|
|
|
|
| |
Since the number of bits is > 0, it is guaranteed that
modulus > 1, not just that modulus > 0.
(Suggested by Jake Waksbaum @jbaum.)
|
|
|
|
| |
The comment says "writable" but it should be "freeable".
|
|
|
| |
Preparation for Coq PR 9725 that may make `eauto` stronger.
|
|
|
|
|
|
| |
The previous check was incomplete for integer literals in base 10.
Bug 26119
|
| |
|
| |
|
| |
|
|
|
|
|
| |
Follow-up to commit fc9bc643. The latest Menhir version compatible
with the current code base is actually 20181113.
|