src/clight/clightLabelling.mli

   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
  22 val add_cost_labels : Clight.program -> Clight.program