Changeset 2395 for src/Cminor

Timestamp:

Oct 12, 2012, 3:33:53 PM (7 years ago)

Author:

campbell

Message:

Proper handling of comparison of pointers off-the-end of an object.
We might need to drop this if the proofs/back-end work is too involved.

File:

• src/Cminor/semantics.ma (modified) (1 diff)

src/Cminor/semantics.ma

@@ -104 +104 @@
     do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
     do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
-    do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
+    do r ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
     OK ? 〈tr1 ⧺ tr2, r〉
 | Mem ty e ⇒ λEnv.