Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 1 | -2/+3 |
|\ | |||||
| * | reorder phases | David Monniaux | 2020-10-16 | 1 | -2/+3 |
| | | |||||
| * | Changing duplicate verifier to be non optional | Cyril SIX | 2020-10-09 | 1 | -1/+1 |
| | | |||||
* | | Merge branch 'kvx-work' into mppa-RTLpathSE | Cyril SIX | 2020-05-28 | 2 | -0/+183 |
|\| | | | | | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework | ||||
| * | automatic date in the html index | Sylvain Boulmé | 2020-05-28 | 1 | -0/+8 |
| | | |||||
| * | add a renumber phase | David Monniaux | 2020-04-30 | 1 | -0/+1 |
| | | |||||
| * | run a separate CSE3 for LICM | David Monniaux | 2020-04-24 | 1 | -1/+3 |
| | | |||||
| * | sync with licm | David Monniaux | 2020-04-23 | 1 | -1/+1 |
| | | |||||
| * | cbn and copyright | David Monniaux | 2020-04-22 | 1 | -0/+10 |
| | | |||||
| * | use cbn in T instead of simpl in T | David Monniaux | 2020-04-22 | 1 | -1/+1 |
| | | |||||
| * | automated writing Compiler.v | David Monniaux | 2020-04-22 | 1 | -8/+79 |
| | | |||||
| * | generate mkpass | David Monniaux | 2020-04-21 | 1 | -1/+13 |
| | | |||||
| * | Require autogen | David Monniaux | 2020-04-21 | 1 | -8/+22 |
| | | |||||
| * | begin scripting the Compiler.v file | David Monniaux | 2020-04-21 | 1 | -0/+62 |
|/ | |||||
* | Revise the "bench" entries of the test suite | Xavier Leroy | 2019-09-17 | 1 | -0/+101 |
| | | | | | | | | 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. | ||||
* | ndfun: add support for guards on patterns | Xavier Leroy | 2019-08-07 | 1 | -5/+16 |
| | | | | | | Syntax is "pat ?? bexpr => action". The whole case is selected only when "pat" matches and then "bexpr" evaluates to "true". | ||||
* | Extend the modorder tool to handle Coq files as well (#54) | Bernhard Schommer | 2018-02-08 | 1 | -7/+9 |
| | | | | | | 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. | ||||
* | Updated PR by removing whitespaces. Bug 17450. | Bernhard Schommer | 2015-10-20 | 1 | -3/+3 |
| | |||||
* | Removed the recdepend again and replaced it by a builtin Make function. | Bernhard Schommer | 2015-02-27 | 1 | -206/+0 |
| | |||||
* | Updated the recdepend tool to avoid printing of ./ at the begining and ↵ | Bernhard Schommer | 2015-02-25 | 1 | -50/+46 |
| | | | | printing duplicated -I flags. | ||||
* | Added a small ocamlfile that calls ocamlfind recursivly over a given directory. | Bernhard Schommer | 2015-02-24 | 1 | -0/+210 |
| | |||||
* | Use String.map instead of reimplementing it ourselves. | Xavier Leroy | 2014-11-22 | 1 | -5/+18 |
| | | | | Avoids warnings with 4.02. | ||||
* | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵ | Xavier Leroy | 2014-11-22 | 1 | -0/+112 |
| | | | | | | produce the executables. configure: add check for GNU make. | ||||
* | Merge of the nonstrict-ops branch: | xleroy | 2012-01-14 | 1 | -0/+231 |
- 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 |