Changeset 2123 for src/ASM/AssemblyProofSplitSplit.ma
- Timestamp:
- Jun 27, 2012, 4:04:14 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplitSplit.ma
r2122 r2123 1 1 include "ASM/AssemblyProofSplit.ma". 2 2 include "common/LabelledObjects.ma". 3 4 definition instruction_has_label ≝5 λid: Identifier.6 λi.7 match i with8 [ Jmp j ⇒ j = id9 | Call j ⇒ j = id10 | Instruction instr ⇒11 match instr with12 [ JC j ⇒ j = id13 | JNC j ⇒ j = id14 | JZ j ⇒ j = id15 | JNZ j ⇒ j = id16 | JB _ j ⇒ j = id17 | JBC _ j ⇒ j = id18 | DJNZ _ j ⇒ j = id19 | CJNE _ j ⇒ j = id20 | _ ⇒ False21 ]22 | _ ⇒ False23 ].24 25 26 definition is_well_labelled_p ≝27 λinstr_list.28 ∀id: Identifier.29 ∀ppc. ∀ppc_ok.30 ∀i.31 fetch_pseudo_instruction instr_list ppc ppc_ok = i →32 instruction_has_label id (\fst i) →33 occurs_exactly_once ASMTag pseudo_instruction id instr_list.34 3 35 4 lemma short_jump_cond_ok:
Note: See TracChangeset
for help on using the changeset viewer.