Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (9 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r1462 r1542  
    22(** This module defines the instrumentation of a [Clight] program. *)
    33
    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 ->
     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 ->
    1314                 Clight.program * string * string * string StringTools.Map.t
    1415
Note: See TracChangeset for help on using the changeset viewer.