source: Deliverables/D2.2/8051/src/clight/clightLabelling.mli @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 787 bytes
RevLine 
[486]1(** This module defines the labelling of a [Clight] program. *)
2
3(** [add_cost_labels prog] inserts some labels to enable
4    cost annotation.
5
6    The labelling of a function proceeds as follows:
7
8    - A label is added at the beginning of the function.
9
10    - For each branching instruction in the function, a cost label is added at
11      the beginning of each branch. The concerned instructions are:
12      - ternary expressions (includind boolean 'and' and 'or' operators that are
13        transformed at this point);
14      - conditionals;
15      - loops;
16      - switches.
17
18    - For each label instruction in the function, a cost label is added after
19      the label, in order to capture loops potentially created by gotos.
20*)
21
22val add_cost_labels : Clight.program -> Clight.program
Note: See TracBrowser for help on using the repository browser.