source: Deliverables/D2.2/8051/src/clight/clightAnnotator.mli @ 1664

Last change on this file since 1664 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

File size: 1.3 KB
Line 
1
2(** This module defines the instrumentation of a [Clight] program. *)
3
4(** [instrument cost_tern prog cost_map] instruments the program [prog]. First a
5    fresh global variable --- the so-called cost variable --- is added to the
6    program. Then, each cost label in the program is replaced by an increment of
7    the cost variable, following the mapping [cost_map]. The function also
8    returns the name of the cost variable, the name of the cost increment
9    function, and a fresh uninitialized global (cost) variable associated to each
10    extern function. [cost_tern] rules whether cost increments are given by
11    ternary expressions (more readable) or by branch statements (for frama-c
12    itegration). *)
13val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
14                 Clight.program * string * string * string StringTools.Map.t
15
16val cost_labels : Clight.program -> CostLabel.Set.t
17val user_labels : Clight.program -> Label.Set.t
18val all_labels  : Clight.program -> StringTools.Set.t
19val all_idents  : Clight.program -> StringTools.Set.t
20
21val fresh_ident : string (* base *) -> Clight.program -> string
22
23val fresh_universe :
24  string (* prefix *) -> Clight.program -> StringTools.Gen.universe
25
26val make_fresh :
27  string (* prefix *) -> Clight.program -> (unit -> string)
Note: See TracBrowser for help on using the repository browser.