Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCostsSplit.ml

    r2601 r2649  
    1919open Fetch
    2020
     21open String
     22
    2123open LabelledObjects
    22 
    23 open Coqlib
    24 
    25 open Floats
    2624
    2725open Arithmetic
     
    3836
    3937open Deqsets
     38
     39open ErrorMessages
    4040
    4141open PreIdentifiers
     
    5656
    5757open Identifiers
    58 
    59 open Char
    60 
    61 open String
    6258
    6359open Extranat
     
    107103let rec traverse_code_internal code_memory cost_labels program_counter0 program_size =
    108104  (match program_size with
    109    | Nat.O -> (fun _ -> Identifiers.empty_map CostLabel.costTag)
     105   | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
    110106   | Nat.S program_size' ->
    111107     (fun _ ->
     
    133129              ASMCosts.block_cost code_memory program_counter0 cost_labels
    134130            in
    135             Identifiers.add CostLabel.costTag (Types.pi1 cost_mapping) lbl
    136               (Types.pi1 cost))) __)) __
     131            Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
     132              lbl (Types.pi1 cost))) __)) __
    137133
    138134(** val traverse_code :
     
    164160  let cost_map = compute_costs p.Types.fst p.Types.snd in
    165161  (fun l_sig ->
    166   Identifiers.lookup_present CostLabel.costTag (Types.pi1 cost_map)
     162  Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
    167163    (StructuredTraces.as_cost_get_label
    168164      (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.Types.fst)
Note: See TracChangeset for help on using the changeset viewer.