Ignore:
Timestamp:
Nov 15, 2011, 5:11:19 PM (9 years ago)
Author:
tranquil
Message:
  • 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:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.mli

    r1291 r1507  
    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 and the name of the cost increment function.
    9                
     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
    1013    TODO: int to expressions *)
    11 val instrument : Clight.program -> int CostLabel.Map.t ->
     14val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
    1215                 Clight.program * string * string
    1316
Note: See TracChangeset for help on using the changeset viewer.