1 (** This module defines the labelling of a [Clight] program. *)
3 (** [add_cost_labels prog] inserts some labels to enable
6 The labelling of a function proceeds as follows:
8 - A label is added at the beginning of the function.
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);
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.
22 val add_cost_labels : Clight.program -> Clight.program