| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|\
| |
| | |
This PR activates more OCaml warnings and turns all warnings into errors. Also some unused functions, variables and types are removed.
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Removed unused code, factored out common functions and added an
interface file.
Bug 18394
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Since the menhir version we use requires ocaml>4.02 we can also
upgrade the required ocaml version to >4.02 and remove the
deprecate String functions.
Also we now activate all warnings except for 4,9 und 27 for regular
code plus a bunch of warnings for the generated code. 4 and 9 are
not really usefull and 27 is deactivated since until the usage
string is printed in a way that requires no newline.
Bug 18394.
|
| | |
| | |
| | |
| | |
| | |
| | | |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
| |/
|/|
| |
| |
| |
| | |
Windows style line endings can end up in the Tokenize pass. This
can lead to some problems for example in pragma processing.
Bug 18316
|
|/
|
|
|
|
|
| |
- Coqlib: option_rel to lift a relation to option type.
- Coqlib: more lemmas about list_forall2.
- Coqlib: introduce type nlist (nonempty lists) and some operations.
- Maps: a variant of PTree.elements_extensional that uses option_rel.
|
| |
|
| |
|
|
|
|
|
|
| |
On windows opening files in text mode can result in errors due to
non-windows compatible input. Thus open files only in binary mode.
Bug 17664
|
| |
|
|
|
|
|
|
| |
Added functions to add more information to the debuging interface,
like the struct layout with offsets, bitifiled layout and removed
the no longer needed mapping from stamp to atom.
|
| |
|
|
|
|
|
|
|
|
|
| |
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).
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| | |
comments.
Refactor printing of .loc debug directives in backend/PrintAnnot.ml
|
|/
|
|
|
| |
Revised parsing of compcert.ini file to split arguments into words
like POSIX shell does (including quotes).
|
| |
|
| |
|
|
|
|
|
| |
Use "elements_remove" to simplify the proof of "cardinal_remove".
Simplify some of the proofs over function "xelements".
|
|
|
|
|
|
|
| |
(Contributed by Vincent Laporte.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2618 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2536 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2520 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
(Merge of branch newparser.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
over booleans.
Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31].
Driver: timer for whole compilation.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) Revised division of labor between RTLtyping and Lineartyping:
- RTLtyping no longer keeps track of single-precision floats,
switches from subtype-based inference to unification-based inference.
- Unityping: new library for unification-based inference.
- Locations: don't normalize at assignment in a stack slot
- Allocation, Allocproof: simplify accordingly.
- Lineartyping: add inference of locations that contain
a single-precision float.
- Stackingproof: adapted accordingly.
This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c).
This corresponds to commits 2435+2436 plus improvements in Lineartyping.
2) Add -dtimings option to measure compilation times.
Moved call to C parser from Elab to Parse, to make it easier to
measure parsing time independently of elaboration time.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
implementation of long <-> float conversions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2430 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2429 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
- endianness
- alignment constraints for 8-byte types
(which is 4 for x86 ABI and 8 for other ABIs)
- NaN handling options (superceding the Nan module, removed).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
VERSION: bump version number.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2379 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2335 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Maps.v: add a PTree.fold1 operation that doesn't maintain the key.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
| |
are necessary, only two parameters (default_pl and choose_binop_pl).
SelectDiv: optimize FP division by a power of 2.
ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2306 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
More precise modeling of NaNs.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
multiply-high and shifts.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
Delight).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
- introduce Float.floatofint{,u} and use it in the semantics of C
- prove that it is equivalent to int->double conversion followed by
double->float rounding, and use this fact to justify code generation
in Cshmgen.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
casts int64 -> float64 -> float32. The latter causes double rounding
errors.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|