Changeset 2101 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 19, 2012, 4:43:50 PM (7 years ago)
Author:
boender
Message:
  • renamed medium to absolute jump
  • revised proofs of policy, some daemons removed
  • reverted earlier change in extralib, bounded quantification now again uses lt
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2081 r2101  
    1212inductive jump_length: Type[0] ≝
    1313  | short_jump: jump_length
    14   | medium_jump: jump_length
     14  | absolute_jump: jump_length
    1515  | long_jump: jump_length.
    1616 
     
    2626      〈eq_bv 9 upper (zero …), false:::lower〉.
    2727 
    28 definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)
     28definition absolute_jump_cond: Word → Word → (*pseudo_instruction →*)
    2929  bool × (BitVector 11) ≝
    3030  λpc_plus_jmp_length.λaddr.(*λinstr.*)
     
    528528    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    529529    let lookup_address ≝ sigma (lookup_labels call) in
    530     let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
     530    let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    531531    let do_a_long ≝ policy ppc in
    532532    if mj_possible ∧ ¬ do_a_long then
     
    549549        [ SJMP address ]
    550550    else
    551       let 〈mj_possible, disp2〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
     551      let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    552552      if mj_possible ∧ ¬ do_a_long then
    553553        let address ≝ ADDR11 disp2 in
Note: See TracChangeset for help on using the changeset viewer.