Ignore:
Timestamp:
Nov 6, 2012, 12:02:13 PM (7 years ago)
Author:
campbell
Message:

Tighten requirements on switch statements in Clight to only give semantics
when the controlling expression's type and values match up and the cases'
labels make sense.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r2391 r2428  
    429429    | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    430430    ]
    431 | #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?);
    432     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     431| #f #e #sl #sl' #k #env #m #sz #sg #i #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     432    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     433    >H2 whd in ⊢ (??%?); @(dec_true … (sz_eq_dec … sz) (refl ??)) #SZ
     434    whd in ⊢ (??%?); >H3
    433435    @refl
    434436| #f #s #k #env #m *; #es >es @refl
Note: See TracChangeset for help on using the changeset viewer.