Ignore:
Timestamp:
Feb 2, 2011, 12:41:05 PM (9 years ago)
Author:
campbell
Message:

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

File:
1 edited

Legend:

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

    r484 r485  
    5757initial_state p s → initial_state p s' → s = s'.
    5858#p s s' H1 H2;
    59 ninversion H1; #b1 f1 e11 e12 e13;
    60 ninversion H2; #b2 f2 e21 e22 e23;
    61 nrewrite > e11 in e21;
    62 #e1; nrewrite > (?:b1 = b2) in e12;
    63 ##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1);
     59ninversion H1; #b1 f1 ge1 m1 e11 e12 e13 e14 e15;
     60ninversion H2; #b2 f2 ge2 m2 e21 e22 e23 e24 e25;
     61nrewrite > e11 in e21; #e1; nrewrite > (?:ge1 = ge2) in e13 e14;
     62##[ ##2: ndestruct (e1) skip (e11); napply refl; ##]
     63#e13 e14;
     64
     65nrewrite > e12 in e22; #e2; ndestruct (e2) skip (e12);
     66
     67nrewrite > e13 in e23; #e3; nrewrite > (?:b1 = b2) in e14;
     68##[ nrewrite > e24; #e4; nrewrite > (?:f2 = f1);
    6469  ##[ //;
    65   ##| ndestruct (e2) skip (e22 e23); //;
     70  ##| ndestruct (e4) skip (e24 e25); //;
    6671  ##]
    67 ##| ndestruct (e1) skip (e11); //
     72##| ndestruct (e3) skip (e13); //
    6873##] nqed.
    6974
     
    7883
    7984ntheorem the_initial_state:
    80   ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
     85  ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
    8186#p s; ncases p; #fns main globs H;
    8287ninversion H;
    83 #b f e1 e2 e3;
     88#b f ge m e1 e2 e3 e4 e5; @ge;
    8489nwhd in ⊢ (??%?);
    8590nrewrite > e1;
    8691nwhd in ⊢ (??%?);
    8792nrewrite > e2;
     93nwhd in ⊢ (??%?);
     94nrewrite > e3;
     95nwhd in ⊢ (??%?);
     96nrewrite > e4;
    8897nwhd; napply refl;
    8998nqed.
Note: See TracChangeset for help on using the changeset viewer.