| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
| |
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).
|
| |
|
|
| |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
| |
|
|
|
|
| |
This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.
|
| |
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
literals.
This is a follow-up to commit 350354c.
- Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse
- Add early checks for overflow and underflow and prove them correct.
- Improve speed of Bparse by using a fast exponentiation (square-and-multiply).
|
| | |
|
|
|
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
