| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
| |
Initially, the "bench" entries of the test suite used a "xtime" utility
developed in-house and not publically available.
This commit adds a version of "xtime" written in OCaml (tools/xtime.ml)
and updates the "bench" entries of the test/*/Makefile to use it.
|
|
|
|
|
|
| |
Syntax is "pat ?? bexpr => action".
The whole case is selected only when "pat" matches and then "bexpr"
evaluates to "true".
|
|
|
|
|
|
| |
This is useful to e.g. identify the .vo files from CompCert that a clightgen-generated .v file needs.
Also: the "result" field of the record type is now initialized with the LHS of the dependency, not the RHS. It doesn't matter because the result field is unused, but it makes more sense now.
|
| |
|
| |
|
|
|
|
| |
printing duplicated -I flags.
|
| |
|
|
|
|
| |
Avoids warnings with 4.02.
|
|
|
|
|
|
| |
produce the executables.
configure: add check for GNU make.
|
|
- Most RTL operators now evaluate to Some Vundef instead of None
when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|