Ignore:
Timestamp:
Mar 19, 2013, 10:21:08 PM (8 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret2.ml

    r2905 r2909  
    163163    ASM.labelled_object_code -> Measurable.preclassified_system **)
    164164let oC_preclassified_system c =
    165   let cm = Fetch.load_code_memory c.ASM.oc in
    166   mk_preclassified_system_of_abstract_status
    167     (ASMCosts.oC_abstract_status cm c.ASM.costlabels) (fun st ->
     165  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
     166    (fun st ->
    168167    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    169168      (Interpret.execute_1 (Fetch.load_code_memory c.ASM.oc) (Obj.magic st)))
    170     (Obj.magic (Status.initialise_status cm))
     169    (Obj.magic (Status.initialise_status (Fetch.load_code_memory c.ASM.oc)))
    171170
    172171open Assembly
     
    213212  | ASM.Mov (x, x0) -> Types.None
    214213
     214(** val aSM_as_result :
     215    ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
     216    Types.option **)
     217let aSM_as_result prog st =
     218  let finaladdr =
     219    Fetch.address_of_word_labels prog.ASM.code prog.ASM.final_label
     220  in
     221  ASMCosts.as_result_of_finaladdr prog st finaladdr
     222
    215223(** val aSM_abstract_status :
    216224    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     
    221229    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
    222230    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
    223     StructuredTraces.as_result = (fun x -> Types.None);
     231    StructuredTraces.as_result = (Obj.magic (aSM_as_result prog));
    224232    StructuredTraces.as_call_ident = (fun x -> Positive.One
    225233    (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
Note: See TracChangeset for help on using the changeset viewer.