Ignore:
Timestamp:
May 14, 2012, 7:56:15 PM (8 years ago)
Author:
sacerdot
Message:

common/StructuredTraces no longer depends on ASM/AbstractStatus (again)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AbstractStatus.ma

    r1939 r1944  
    22include "ASM/Status.ma".
    33include "ASM/Fetch.ma".
     4include "common/StructuredTraces.ma".
    45
    56include "basics/lists/listb.ma".
    6 
    7 inductive status_class: Type[0] ≝
    8   | cl_return: status_class
    9   | cl_jump: status_class
    10   | cl_call: status_class
    11   | cl_other: status_class.
    127
    138definition ASM_classify00: ∀a. preinstruction a → status_class ≝
     
    7570  λs: Status code_memory.
    7671    ASM_classify0 (current_instruction … s).
    77 
    78 record abstract_status : Type[1] ≝
    79 {
    80     as_status :> Type[0]
    81   ; as_execute : as_status → as_status → Prop
    82   ; as_pc : DeqSet
    83   ; as_pc_of : as_status → as_pc
    84   ; as_classifier : as_status → status_class → Prop
    85   ; as_label : as_status → option costlabel
    86   ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    87   ; as_final: as_status → Prop
    88 }.
Note: See TracChangeset for help on using the changeset viewer.