Ignore:
Timestamp:
Jul 24, 2012, 7:40:21 PM (8 years ago)
Author:
campbell
Message:

Add new invariant to Cminor that return typs should be respected.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r2232 r2251  
    395395| 7,8:
    396396  @(stmt_P_mp … (f_inv f))
    397   #s * #V #L %
     397  #s * #V #L #R %
    398398  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
    399399    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
Note: See TracChangeset for help on using the changeset viewer.