Changeset 2175


Ignore:
Timestamp:
Jul 10, 2012, 6:08:35 PM (5 years ago)
Author:
tranquil
Message:

corrected small bug

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL_paolo.ma

    r2174 r2175  
    2727(* Paolo: I'm changing the following: before, spilled registers were
    2828  assigned stack addresses going from SP + #frame_size - #stack_params
    29   excluded down to SP excluded. I am turning it upside down, so that
     29  excluded down to SP included. I am turning it upside down, so that
    3030  the offset does not need the stack size to be computed *)
    31 definition adjust_off ≝
    32   λoff.
    33   \snd (half_add ? int_size off).
    3431
    3532definition preserve_carry_bit :
     
    4138  ∀globals.Byte → list (joint_seq ltl_params globals) ≝
    4239  λglobals,off.
    43   [ 𝐀 ← adjust_off off
     40  [ 𝐀 ← off
    4441  ; 𝐀 ← 𝐀 .Add. RegisterSPL
    4542  ; RegisterDPL ← 𝐀
Note: See TracChangeset for help on using the changeset viewer.