src/clight/clightAnnotator.mli

   1
   2 (** This module defines the instrumentation of a [Clight] program. *)
   3
   4 (** [instrument prog cost_map] instruments the program [prog]. First a fresh
   5     global variable --- the so-called cost variable --- is added to the program.
   6     Then, each cost label in the program is replaced by an increment of the cost
   7     variable, following the mapping [cost_map]. The function also returns the
   8     name of the cost variable, the name of the cost increment function, and a
   9     fresh uninitialized global (cost) variable associated to each extern
  10     function. *)
  11
  12 val instrument : Clight.program -> int CostLabel.Map.t ->
  13                  Clight.program * string * string * string StringTools.Map.t
  14
  15 val cost_labels : Clight.program -> CostLabel.Set.t
  16 val user_labels : Clight.program -> Label.Set.t
  17 val all_labels  : Clight.program -> StringTools.Set.t
  18 val all_idents  : Clight.program -> StringTools.Set.t
  19
  20 val fresh_ident : string (* base *) -> Clight.program -> string
  21
  22 val fresh_universe :
  23   string (* prefix *) -> Clight.program -> StringTools.Gen.universe
  24
  25 val make_fresh :
  26   string (* prefix *) -> Clight.program -> (unit -> string)
  27
  28
  29 (** utils *)
  30 val names : Clight.program -> StringTools.Set.t