Changeset 2907 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Mar 19, 2013, 7:48:19 PM (7 years ago)
Author:
sacerdot
Message:
  1. a few bugs fixed
  2. as_return implemented for ASM & OC
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r2905 r2907  
    3939definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    4040 λc:labelled_object_code.
    41   let cm ≝ load_code_memory (oc c) in
    4241  mk_preclassified_system_of_abstract_status
    4342   labelled_object_code
    44    (OC_abstract_status cm (costlabels c))
     43   (OC_abstract_status c)
    4544   (λst. return (execute_1 … st))
    46    (initialise_status … cm).
     45   (initialise_status … (load_code_memory (oc c))).
    4746
    4847(* Pre-classified system for ASM *)
     
    101100qed.
    102101
     102definition ASM_as_result: ∀prog. PseudoStatus prog → option int ≝
     103 λprog,st.
     104  let finaladdr ≝ address_of_word_labels (code prog) (final_label … prog) in
     105   as_result_of_finaladdr … st finaladdr.
     106
    103107definition ASM_abstract_status:
    104108 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
     
    112116      (ASM_as_label_of_pc prog …)
    113117      (ASM_next_instruction_properly_relates_program_counters prog)
    114       ? (* (λs.False) *)
     118      (ASM_as_result …)
    115119      ?
    116120      ?.
    117   #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
     121  #x cases daemon (* XXX: (tail)call_ident function *)
    118122qed.
    119123
Note: See TracChangeset for help on using the changeset viewer.