Ignore:
Timestamp:
Jun 27, 2012, 4:04:14 PM (8 years ago)
Author:
boender
Message:
File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplitSplit.ma

    r2122 r2123  
    11include "ASM/AssemblyProofSplit.ma".
    22include "common/LabelledObjects.ma".
    3 
    4 definition instruction_has_label ≝
    5   λid: Identifier.
    6   λi.
    7   match i with
    8   [ Jmp j ⇒ j = id
    9   | Call j ⇒ j = id
    10   | Instruction instr ⇒
    11     match instr with
    12     [ JC j ⇒ j = id
    13     | JNC j ⇒ j = id
    14     | JZ j ⇒ j = id
    15     | JNZ j ⇒ j = id
    16     | JB _ j ⇒ j = id
    17     | JBC _ j ⇒ j = id
    18     | DJNZ _ j ⇒ j = id
    19     | CJNE _ j ⇒ j = id
    20     | _ ⇒ False
    21     ]
    22   | _ ⇒ False
    23   ].
    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.
    343
    354lemma short_jump_cond_ok:
Note: See TracChangeset for help on using the changeset viewer.