Changeset 2263 for src/Clight/Csem.ma


Ignore:
Timestamp:
Jul 25, 2012, 6:55:36 PM (8 years ago)
Author:
garnier
Message:

Finished proving semantics preservation under memory injections for unary and binary ops. Had to tweak a definition in Csem.ma to circumvent lack of unfold.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2177 r2263  
    327327let rec sem_cmp (c:comparison)
    328328                  (v1: val) (t1: type) (v2: val) (t2: type)
    329                   (m: mem): option val ≝
     329                  (m: mem) on m: option val ≝
    330330  match classify_cmp t1 t2 with
    331331  [ cmp_case_ii _ sg ⇒
Note: See TracChangeset for help on using the changeset viewer.