Changeset 2395 for src/Cminor


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r2254 r2395  
    104104    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
    105105    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
    106     do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
     106    do r ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
    107107    OK ? 〈tr1 ⧺ tr2, r〉
    108108| Mem ty e ⇒ λEnv.
Note: See TracChangeset for help on using the changeset viewer.