Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |