Ignore:
Timestamp:
Apr 6, 2013, 7:35:25 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/fetch.mli

    r2999 r3106  
    11open Preamble
     2
     3open Types
     4
     5open Hints_declaration
     6
     7open Core_notation
     8
     9open Pts
     10
     11open Logic
     12
     13open Jmeq
     14
     15open Russell
    216
    317open Exp
     
    1529open Div_and_mod
    1630
    17 open Jmeq
    18 
    19 open Russell
    20 
    21 open Types
    22 
    2331open List
    2432
     
    2836
    2937open Bool
    30 
    31 open Hints_declaration
    32 
    33 open Core_notation
    34 
    35 open Pts
    36 
    37 open Logic
    3838
    3939open Relations
     
    7979open ASM
    8080
    81 val inefficient_address_of_word_labels_code_mem :
    82   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
     81val inefficient_address_of_label :
     82  ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat
    8383
    8484type label_map = Nat.nat Identifiers.identifier_map
    8585
    8686val create_label_cost_map0 :
    87   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    88   BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
     87  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     88  Types.prod Types.sig0
    8989
    9090val create_label_cost_map :
    91   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    92   BitVectorTrie.bitVectorTrie) Types.prod
     91  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     92  Types.prod
    9393
    9494val address_of_word_labels :
    9595  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
    96 
    97 val bitvector_max_nat : Nat.nat -> Nat.nat
    98 
    99 val code_memory_size : Nat.nat
    10096
    10197val prod_inv_rect_Type0 :
Note: See TracChangeset for help on using the changeset viewer.