Changeset 2015 for src/ASM/Assembly.ma
- Timestamp:
- Jun 4, 2012, 4:06:56 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2005 r2015 418 418 qed. 419 419 420 (* XXX: pc_plus_sjmp_length used to be just sigma of ppc. This is incorrect 421 as relative lengths are computed from the *end* of the SJMP, not from 422 the beginning. This caused a mismatch with Jaap's code which was 423 computing the lengths correctly, and has not been fixed. 424 *) 420 425 definition expand_relative_jump_internal: 421 426 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word. … … 425 430 λlookup_labels.λsigma.λlbl.λppc,i. 426 431 let lookup_address ≝ sigma (lookup_labels lbl) in 427 let pc ≝ sigma ppcin428 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in432 let pc_plus_sjmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 433 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_sjmp_length lookup_address false in 429 434 let 〈upper, lower〉 ≝ split ? 8 8 result in 430 435 if eq_bv ? upper (zero 8) then
Note: See TracChangeset
for help on using the changeset viewer.