Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (9 years ago)
Author:
ayache
Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File:
1 edited

Legend:

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

    r818 r1462  
    66    Then, each cost label in the program is replaced by an increment of the cost
    77    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. *)
     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. *)
    911
    1012val instrument : Clight.program -> int CostLabel.Map.t ->
    11                  Clight.program * string * string
     13                 Clight.program * string * string * string StringTools.Map.t
    1214
    1315val cost_labels : Clight.program -> CostLabel.Set.t
Note: See TracChangeset for help on using the changeset viewer.