Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | begin implementing -fcse3-conditions | David Monniaux | 2020-12-09 | 1 | -0/+3 |
| | |||||
* | new option for CSE3 (trivial ops) | David Monniaux | 2020-10-27 | 1 | -0/+3 |
| | |||||
* | Changing duplicate verifier to be non optional | Cyril SIX | 2020-10-09 | 1 | -3/+0 |
| | |||||
* | -fcse3-glb | David Monniaux | 2020-05-06 | 1 | -0/+3 |
| | |||||
* | CSE3 across merges | David Monniaux | 2020-05-06 | 1 | -0/+3 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-23 | 1 | -1/+4 |
|\ | |||||
| * | CSE3 across calls | David Monniaux | 2020-04-23 | 1 | -1/+4 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-20 | 1 | -0/+6 |
|\| | |||||
| * | add options for controlling madd and notrap selection | David Monniaux | 2020-04-19 | 1 | -0/+3 |
| | | |||||
| * | begin adapting for LICM phase | David Monniaux | 2020-04-01 | 1 | -0/+3 |
| | | |||||
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-licm | David Monniaux | 2020-04-01 | 1 | -2/+1 |
| |\ | |||||
* | \ | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features | David Monniaux | 2020-04-12 | 1 | -0/+6 |
|\ \ \ | |||||
| * | | | reloading and exploiting seems to work | David Monniaux | 2020-04-08 | 1 | -0/+3 |
| | | | | |||||
| * | | | begin installing profiling | David Monniaux | 2020-04-08 | 1 | -0/+3 |
| | |/ | |/| | |||||
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3 | David Monniaux | 2020-04-01 | 1 | -2/+1 |
|\| | | |/ |/| | |||||
| * | -fduplicate -1 really desactivates the pass in Coq now | Cyril SIX | 2020-04-01 | 1 | -2/+1 |
| | | |||||
* | | CSE3 alias analysis | David Monniaux | 2020-03-14 | 1 | -0/+3 |
| | | |||||
* | | starts compiling but still fake | David Monniaux | 2020-03-10 | 1 | -0/+3 |
|/ | |||||
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 1 | -0/+4 |
|\ | |||||
| * | Added a flag to desactivate tail duplication | Cyril SIX | 2020-01-27 | 1 | -0/+4 |
| | | |||||
* | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2 | David Monniaux | 2020-01-28 | 1 | -0/+3 |
|\ \ | |/ |/| | |||||
| * | connected (just a silly problem) | David Monniaux | 2020-01-28 | 1 | -0/+3 |
| | | |||||
* | | connect forward-moves to compiler | David Monniaux | 2020-01-08 | 1 | -0/+3 |
| | | |||||
* | | to v3.6 | David Monniaux | 2019-09-20 | 1 | -1/+5 |
| | | |||||
* | | -fall-loads-nontrap | David Monniaux | 2019-09-09 | 1 | -0/+3 |
| | | |||||
* | | option -faddx (off by default until questions cleared) | David Monniaux | 2019-05-11 | 1 | -3/+6 |
| | | |||||
* | | -fcoalesce-mem | David Monniaux | 2019-05-03 | 1 | -0/+3 |
| | | |||||
* | | command line options (still incomplete) | David Monniaux | 2019-05-02 | 1 | -0/+9 |
| | | |||||
* | | -fpostpass-ilp | David Monniaux | 2019-03-12 | 1 | -3/+0 |
| | | |||||
* | | Added a flag for changing the scheduler (not any choice available right now) | Cyril SIX | 2019-03-12 | 1 | -0/+3 |
| | | |||||
* | | -O0 will not perform postpass scheduling | Cyril SIX | 2019-01-18 | 1 | -0/+3 |
|/ | |||||
* | Track the locations of local variables using EF_debug annotations. | Xavier Leroy | 2015-08-23 | 1 | -0/+3 |
| | | | | | | | | | | | | | | SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known. | ||||
* | Add flags to control individual optimization passes + flag -O0 for turning ↵ | Xavier Leroy | 2014-11-16 | 1 | -1/+10 |
| | | | | them off. | ||||
* | ARM port: add support for Thumb2. To be tested. | xleroy | 2014-07-27 | 1 | -1/+2 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Add option -Os to optimize for code size rather than for execution speed. | xleroy | 2014-02-19 | 1 | -0/+33 |
Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |