Changeset 3265 for src/LIN


Ignore:
Timestamp:
May 10, 2013, 6:21:46 PM (7 years ago)
Author:
tranquil
Message:

added validate_pointer filter
in Interference added that intereference only fires on non eliminable
statements

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3261 r3265  
    9494  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
    9595  (* eval_ext_seq       ≝ *) (eval_LTL_LIN_ext_seq ?)
    96   (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st)).
     96  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st))
     97  (* validate_pointer   ≝ *) (λ_.λ_.λ_.λ_.λ_.return it).
Note: See TracChangeset for help on using the changeset viewer.