Ignore:
Timestamp:
Mar 8, 2013, 3:51:18 PM (7 years ago)
Author:
tranquil
Message:
  • corrected bug in ERTL semantics (both delframe and newframe did the same operation on the stack pointer...)
  • split RTL semantics in two (one with multiple stack spaces per call, one with only one for all)
  • joint_if_entry is not required anymore to be in the code (as it is covered by entry_costed in good_if)
  • temporarily replaced the two biggest proofs of linearise by daemons
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2807 r2823  
    122122   [ ertl_new_frame ⇒
    123123      ! sp ← sp … st ;
    124       let newsp ≝ shift_pointer … sp framesize in
     124      let newsp ≝ neg_shift_pointer … sp framesize in
    125125      return set_sp … newsp st
    126126   | ertl_del_frame ⇒
Note: See TracChangeset for help on using the changeset viewer.