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/abstractStatus.ml

    r2905 r3106  
    161161| ASM.RealInstruction pre -> aSM_classify00 pre
    162162
    163 (** val current_instruction0 :
    164     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    165     ASM.instruction **)
    166 let current_instruction0 code_memory program_counter =
    167   (Fetch.fetch code_memory program_counter).Types.fst.Types.fst
    168 
    169163(** val current_instruction :
    170164    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
    171165    ASM.instruction **)
    172166let current_instruction code_memory s =
    173   current_instruction0 code_memory s.Status.program_counter
     167  (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst
    174168
    175169(** val current_instruction_label :
    176     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    177     BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
    178     Types.option **)
     170    BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
     171    Status.status -> CostLabel.costlabel Types.option **)
    179172let current_instruction_label code_memory cost_labels s =
    180173  let pc = s.Status.program_counter in
Note: See TracChangeset for help on using the changeset viewer.