Changeset 2047 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 12, 2012, 2:18:16 PM (7 years ago)
Author:
mulligan
Message:

Big bugs in policy calculations found. Waiting for Jaap's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2032 r2047  
    430430   let lookup_address ≝ sigma (lookup_labels lbl) in
    431431   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    432    let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
     432   let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in
    433433   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    434434   if eq_bv ? upper (zero 8) then
     
    553553    let do_a_long ≝ policy ppc in
    554554    let lookup_address ≝ sigma (lookup_labels jmp) in
    555     let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
     555    let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in
    556556    let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    557557    if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
Note: See TracChangeset for help on using the changeset viewer.