Changeset 389


Ignore:
Timestamp:
Dec 8, 2010, 12:18:35 PM (9 years ago)
Author:
campbell
Message:

Sort out minor inconsistency between semantics.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r388 r389  
    10011001  [ Kcall r f e k' ⇒
    10021002    match r with
    1003     [ None ⇒
    1004       match res with
    1005       [ Vundef ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
    1006       | _ ⇒ Wrong ???
    1007       ]
     1003    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
    10081004    | Some r' ⇒
    10091005      match r' with [ mk_pair l ty ⇒
     
    11451141##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
    11461142    #r f e k; nwhd in ⊢ (?????%); ncases r;
    1147   ##[ ncases v; nwhd; //;
     1143  ##[ nwhd; //;
    11481144  ##| #x; ncases x; #y; ncases y; #z; ncases z; #pcl b ofs ty;
    11491145    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
  • C-semantics/CexecIOcomplete.ma

    r388 r389  
    469469    nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?);
    470470    napply refl
    471 ##| #v f env k m; nwhd in ⊢ (??%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
     471##| #v f env k m; napply refl
    472472##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
    473473    nrewrite > H; napply refl
Note: See TracChangeset for help on using the changeset viewer.