Changeset 2395 for src/RTLabs


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/RTLabs/semantics.ma

    r2296 r2395  
    105105      ! v1 ← reg_retrieve (locals f) src1;
    106106      ! v2 ← reg_retrieve (locals f) src2;
    107       ! v' ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
     107      ! v' ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
    108108      ! locals ← reg_store dst v' (locals f);
    109109      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
Note: See TracChangeset for help on using the changeset viewer.