]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/cminor/cminorLabelling.mli
Package description and copyright added.
[pkg-cerco/acc.git] / src / cminor / cminorLabelling.mli
1
2 (** This module defines the labelling of a [Cminor] program. *)
3
4 (** [add_cost_labels prog] inserts some labels to enable
5     cost annotation. 
6
7     The labelling of a function proceeds as follows:
8
9     - A label is added at the beginning of the function.
10
11     - For each branching instruction in the function, a cost label is added at
12       the beginning of each branch. The concerned instructions are:
13       - ternary expressions;
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
22 val add_cost_labels : Cminor.program -> Cminor.program