Changeset 468


Ignore:
Timestamp:
Jan 21, 2011, 10:02:21 AM (7 years ago)
Author:
campbell
Message:

Missing changes to completeness proof for function pointer type fix.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r399 r468  
    369369    nrewrite > (yields_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?);
    370370    nrewrite > H3; nwhd in ⊢ (??%?);
    371     nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
     371    nrewrite > H4; nelim (assert_type_eq_true (fun_typeof e)); #pty ety; nrewrite > ety;
    372372    napply refl;
    373373##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
     
    375375    nrewrite > (yields_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?);
    376376    nrewrite > H4; nwhd in ⊢ (??%?);
    377     nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
     377    nrewrite > H5; nelim (assert_type_eq_true (fun_typeof ef)); #pty ety; nrewrite > ety;
    378378    nwhd in ⊢ (??%?);
    379379    nrewrite > (yields_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
     
    409409##| #f e s k env m; napply refl;
    410410##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (??%?); ncases (is_Sskip s1);
    411     ##[ #H; napply False_ind; /2/;
     411    ##[ #H; napply False_ind; napply (absurd ? H nskip)
    412412    ##| #H; nwhd in ⊢ (??%?); napply refl ##]
    413413##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.