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

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

Started branch of untrusted compiler with indexed labels

  • added indexing structure to CostLabel?
  • propagated changes to other modules
  • added indexing as parameter to labelling
  • loop indexes not implemented yet, so behaviour is still the same
File size: 1.0 KB
Line 
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 and the name of the cost increment function.
9               
10    TODO: int to expressions *)
11val instrument : Clight.program -> int CostLabel.Map.t ->
12                 Clight.program * string * string
13
14val cost_labels : Clight.program -> CostLabel.Set.t
15val user_labels : Clight.program -> Label.Set.t
16val all_labels  : Clight.program -> StringTools.Set.t
17val all_idents  : Clight.program -> StringTools.Set.t
18
19val fresh_ident : string (* base *) -> Clight.program -> string
20
21val fresh_universe :
22  string (* prefix *) -> Clight.program -> StringTools.Gen.universe
23
24val make_fresh :
25  string (* prefix *) -> Clight.program -> (unit -> string)
Note: See TracBrowser for help on using the repository browser.