Ignore:
Timestamp:
Oct 7, 2011, 1:48:26 PM (9 years ago)
Author:
tranquil
Message:

indexing branch is compiling again:

  • clight interpreter updated
  • clight labeller yet to be completed with single-entry loop detection
File:
1 edited

Legend:

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

    r1310 r1319  
    2121type indexing = sexpr list
    2222
    23 type const_indexing = int ref list
     23type const_indexing = int array
    2424
    2525(** [enter_loop n indexing] is used to update indexing when one is entering a
    2626    loop indexed by [n].
    2727        The function recycles the same constant indexing *)
    28 val enter_loop : index option -> const_indexing -> const_indexing
     28val enter_loop : index option -> const_indexing -> unit
    2929
    3030(** [continue_loop n indexing] is used to update indexing when one is continuing a
    3131    loop indexed by [n]. *)
    32 val continue_loop : index option -> const_indexing -> const_indexing
     32val continue_loop : index option -> const_indexing -> unit
    3333
    34 (** [id_indexing n] generates an identity indexing nested in [n] loops *)
    35 val id_indexing : int -> indexing
     34(** [empty_indexing] generates an empty indexing *)
     35val empty_indexing : indexing
    3636
    37 (** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *)
    38 val compose_index : index -> sexpr -> indexing -> indexing
    39 
    40 (** [compose_index l m] applies all the transformations in  [l] to [m] *)
    41 val compose_indexing : indexing -> indexing -> indexing
    42 
    43 val compose_const_indexing : const_indexing -> indexing -> int list
     37(** [add_id_indexing ind] adds an identity mapping in front of ind **)
     38val add_id_indexing : indexing -> indexing
    4439
    4540module IndexingSet : Set.S with type elt = indexing
     
    4944        i : indexing
    5045}
     46
     47val apply_const_indexing : const_indexing -> t -> t
     48
    5149
    5250(** [string_of_cost_label pref t] converts an indexed label to a
Note: See TracChangeset for help on using the changeset viewer.