Changeset 1938 for src/ASM/Interpret.ma
- Timestamp:
- May 14, 2012, 10:05:36 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r1935 r1938 2 2 include "ASM/StatusProofs.ma". 3 3 include "ASM/Fetch.ma". 4 include "common/StructuredTraces.ma". 4 5 5 6 definition sign_extension: Byte → Word ≝ … … 119 120 include alias "arithmetics/nat.ma". 120 121 include alias "ASM/BitVectorTrie.ma". 121 122 inductive status_class : Type[0] ≝123 | cl_return : status_class124 | cl_jump : status_class125 | cl_call : status_class126 | cl_other : status_class.127 122 128 123 definition ASM_classify00: ∀a. preinstruction a → status_class ≝
Note: See TracChangeset
for help on using the changeset viewer.