Ignore:
Timestamp:
Nov 6, 2012, 12:02:13 PM (8 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/CexecEquiv.ma

    r2391 r2428  
    522522  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
    523523  | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    524   | @err2_does_not_interact #x1 #x2 cases x1; //;
     524  | @err2_does_not_interact * // #x1 #x2 #x3 cases (typeof a) // #x4 #x5 whd nodelta in ⊢ (???%); cases (sz_eq_dec ??) // #x6 cases (select_switch ???) //
    525525  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
    526526      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
Note: See TracChangeset for help on using the changeset viewer.