Changeset 2123 for src/ASM/ASM.ma


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

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2032 r2123  
    450450definition assembly_program ≝ list instruction.
    451451definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
     452
     453(* labels & instructions *)
     454definition instruction_has_label ≝
     455  λid: Identifier.
     456  λi.
     457  match i with
     458  [ Jmp j ⇒ j = id
     459  | Call j ⇒ j = id
     460  | Instruction instr ⇒
     461    match instr with
     462    [ JC j ⇒ j = id
     463    | JNC j ⇒ j = id
     464    | JZ j ⇒ j = id
     465    | JNZ j ⇒ j = id
     466    | JB _ j ⇒ j = id
     467    | JBC _ j ⇒ j = id
     468    | DJNZ _ j ⇒ j = id
     469    | CJNE _ j ⇒ j = id
     470    | _ ⇒ False
     471    ]
     472  | _ ⇒ False
     473  ].
Note: See TracChangeset for help on using the changeset viewer.