source: Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.mli @ 1507

Last change on this file since 1507 was 1507, checked in by tranquil, 8 years ago
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File size: 1.2 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 and the name of the cost increment
9    function. [cost_tern] rules whether cost increments are given by ternary
10    expressions (more readable) or by branch statements (for frama-c
11    itegration).
12
13    TODO: int to expressions *)
14val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
15                 Clight.program * string * string
16
17val cost_labels : Clight.program -> CostLabel.Set.t
18val user_labels : Clight.program -> Label.Set.t
19val all_labels  : Clight.program -> StringTools.Set.t
20val all_idents  : Clight.program -> StringTools.Set.t
21
22val fresh_ident : string (* base *) -> Clight.program -> string
23
24val fresh_universe :
25  string (* prefix *) -> Clight.program -> StringTools.Gen.universe
26
27val make_fresh :
28  string (* prefix *) -> Clight.program -> (unit -> string)
Note: See TracBrowser for help on using the repository browser.