WCET-Oriented Loop Bound Analysis is built on top of the C CompCert verified compiler via the addition of a function that performs the loop bound computation and outputs the results of the analysis. These results can, for instance, be used by WCET tools to estimate the WCET of the program.

To contact any of the authors (Sandrine Blazy, Andre Maroneze and David Pichardie), send an e-mail to

The main theorems listed in the paper can be found at the following files:

- Theorem 1 (main theorem) - bound_correct: GlobalBounds_proof
- Theorem 2 (start-to-end correctness) - transf_c_program_with_bound_correct: Main
- Theorem 3 (soundness of program slicing) - program_slicing_is_sound: WCETSlice
- Theorem 4 (termination of program slicing) - slicing_preserves_termination: WCETSlice

(tested with OCaml 4.00 and Coq 8.3pl5).

- Download and extract the loopbound archive (tar xvf loopbound.tgz)
- Inside the loopbound directory, run make all (optionally add -j4 for parallel processing) to Coq-prove all files, to extract the OCaml code and to compile it (this will take several minutes).
- Run make benchs to launch the analysis on a subset of the Mälardalen WCET benchmarks, displaying the obtained global bounds for each loop. Each loop is identified by its header node on the RTL language.

Afterwards, you can run rtlcomp -loopbounds <file> on a specific C program to analyze it.

Adding option -localbounds to rtlcomp prints information about local loop bounds. You can therefore run rtlcomp -loopbounds -localbounds <file> on a C program. Running make benchs.debug will run all benchmarks with this extra flag.

To insert annotations such as the ones in the paper, you need to use CompCert's
syntax for annotations: __builtin_annot("id"),
where id is a string containing an unique identifier
of your choice (note that, if you reuse an identifier, the result associated to
it will be the sum of the executions of all program points containing the
identifier, but it will still be a correct bound).

Annotations can be placed at any program point. For instance, consider the
following example program:

int main() { int _reg_vint = 0; /* always add this line at the beginning of the main function */ int i = 0; __builtin_annot("entry"); do { i++; __builtin_annot("loop"); } while (i < 5); __builtin_annot("exit"); return 0; }Running ccomp -bounds <file> will produce the following result:

Annotation bounds (3 annotations): exit -> Some (1) entry -> Some (1) loop -> Some (5)Note: running ccomp -bounds <file> on a file that does not contain any annotations will not produce any output. To automatically bound all program loops, use rtlcomp -loopbounds <file> instead.

The documentation gives a commented listing of the Coq
specifications and proofs for the main development files.

Proof scripts are folded by default, but
can be viewed by clicking on "Proof".

- Bourdoncle: Type of a Bourdoncle component.
- Counter: Counters for the instrumented semantics.
- VarsUseDef: Specification of def/use sets for RTL instructions.
- RTLWfFunction: Well-formed RTL function validator.
- RTLPaths: Definitions and lemmas related to paths in the CFG of a well-formed function.
- Scope: Scopes: definition, validation and construction.
- CountingSem: Instrumented semantics with iteration counters.
- CountingSem_proof: Correctness of the instrumented semantics.
- LightLive: Liveness analysis over RTL.
- SliceGen: Validates a set of slice nodes and produces an executable sliced function.
- SliceObs_proof: Lemmas related to the observable vertices validator.
- SliceRelVar_proof: Lemmas related to relevant variables.
- SliceScopeExits_proof: Lemmas related to SliceScopeExits.
- Sliceproof: Several lemmas related to program slicing.
- SliceAgree: Lemmas about agreement between relevant variables.
- WeakSimulation: Definition of a weak simulation for a small-step semantics.
- WCETSlice: Correctness proof for the program slicing.
- LocalBounds: Computation and correctness proof of local bounds.
- HeaderBounds: Correctness proof of header bounds.
- GlobalBounds: Computation of global bounds.
- GlobalBounds_proof: Correctness proof of global bounds.
- Main: Start-to-end correctness proof.