Changeset 3265 for src/LIN

Timestamp:

May 10, 2013, 6:21:46 PM (8 years ago)

Author:

tranquil

Message:

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

File:

• src/LIN/joint_LTL_LIN_semantics.ma (modified) (1 diff)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -94 +94 @@
   λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
   (* eval_ext_seq       ≝ *) (eval_LTL_LIN_ext_seq ?)
-  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st)).
+  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st))
+  (* validate_pointer   ≝ *) (λ_.λ_.λ_.λ_.λ_.return it).