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

Last change on this file since 1507 was 1507, checked in by tranquil, 9 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: 622 bytes
Line 
1type cond =
2    | Ceq of int         (** index is equal to *)
3    | Cgeq of int        (** index is greater or equal to *)
4    | Cmod of int*int    (** index modulo equal to *)
5    | Cgeqmod of int*int*int (** index greater than and modulo equal to *)
6
7module CondSet : Set.S with type elt = cond
8
9open CostLabel
10
11type cost_expr =
12    | Exact of int
13    | Ternary of index * CondSet.t * cost_expr * cost_expr
14
15(** [expr_cost_mapping_of_cost_mapping] turns a cost mapping on indexed
16    labels into a mapping from cost atoms to cost expressions *)
17val cost_expr_mapping_of_cost_mapping : int Map.t -> cost_expr Atom.Map.t
18
Note: See TracBrowser for help on using the repository browser.