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/CexecSound.ma

    r2391 r2428  
    428428    ]
    429429  | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv
    430     @step_switch @(exec_expr_sound' … Hv)
     430    lapply (refl ? (typeof ex)) cases (typeof ex) in ⊢ (???% → %); // #sz' #sg #TY
     431    whd in ⊢ (?????%); cases (sz_eq_dec sz sz') // #SZ destruct (SZ)
     432    whd in ⊢ (?????%); @opt_bindIO_OK #ls' #LS
     433    @(step_switch … TY LS) @(exec_expr_sound' … Hv)
    431434  | #l #s' //
    432435  | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
Note: See TracChangeset for help on using the changeset viewer.