Changeset 2018 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jun 5, 2012, 5:49:09 PM (7 years ago)
Author:
mulligan
Message:

CJNE case a complete mess.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2008 r2018  
    341341    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)
    342342                    + added in
    343     if leb (addr - \fst inc_sigma) 126
     343    if leb (addr - \fst inc_sigma) 129
    344344    then short_jump
    345345    else long_jump
    346346  else
    347347    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    348     if leb (\fst inc_sigma - addr) 129
     348    if leb (\fst inc_sigma - addr) 125
    349349    then short_jump
    350350    else long_jump.
Note: See TracChangeset for help on using the changeset viewer.