Changeset 2428 for src/Clight/Cexec.ma


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

    r2391 r2428  
    461461  | Sswitch a sl ⇒
    462462      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    463       match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
    464                    | _ ⇒ Wrong ??? (msg TypeMismatch)]
     463      match v with
     464      [ Vint sz n ⇒
     465        match typeof a with
     466        [ Tint sz' _ ⇒
     467          match sz_eq_dec sz sz' with
     468          [ inl _ ⇒
     469            ! sl' ← opt_to_io … (msg TypeMismatch) (select_switch sz n sl);
     470            ret ? 〈tr, State f (seq_of_labeled_statement sl') (Kswitch k) e m〉
     471          | _ ⇒ Wrong ??? (msg TypeMismatch)
     472          ]
     473        | _ ⇒ Wrong ??? (msg TypeMismatch)
     474        ]
     475      | _ ⇒ Wrong ??? (msg TypeMismatch)]
    465476  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
    466477  | Sgoto lbl ⇒
Note: See TracChangeset for help on using the changeset viewer.