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

    r399 r485  
    948948  ¬ ∃r.final_state s r.
    949949#ge s H; ncases H;
    950 #b f E1 E2; @; *; #r H2;
     950#b f ge m E1 E2 E3 E4; @; *; #r H2;
    951951ninversion H2;
    952 #r' m E3 E4; ndestruct (E3);
     952#r' m' E5 E6; ndestruct (E5);
    953953nqed.
    954954
     
    972972   ∃b.execution_matches_behavior e b ∧ exec_program p b.
    973973#classic constructive_indefinite_description p e;
    974 nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
     974nwhd in ⊢ (?%? → ??(λ_.?(?%?)%));
    975975nlapply (make_initial_state_sound p);
    976976nlapply (the_initial_state p);
    977977ncases (make_initial_state p);
    978 ##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?(??%)? → ?);
     978##[ #gs; ncases gs; #ge s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?%? → ?);
     979    ncases INITIAL; #Ege INITIAL'';
    979980    nrewrite > (exec_inf_aux_unfold …);
    980981    nwhd in ⊢ (?%? → ?);
    981982    ncases (is_final_state s);
    982983    ##[ #F; napply False_ind;
    983         napply (absurd ?? (initial_state_not_final … INITIAL));
     984        napply (absurd ?? (initial_state_not_final … INITIAL''));
    984985        ncases F; #r F'; @r; napply F';
    985986    ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e;
     
    989990              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
    990991        *; #b MATCHES; @b; @; //;
     992        #ge'; nrewrite > Ege; #Ege'; nrewrite > (?:ge' = ge); ##[ ##2: ndestruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ##]
    991993        ninversion MATCHES;
    992994        ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM;
     
    995997            nrewrite > E1 in TERM; #TERM;
    996998            napply (program_terminates (mk_transrel … step) ?? ge s);
    997             ##[ ##2: napply INITIAL
     999            ##[ ##2: napply INITIAL''
    9981000            ##| ##3: napply (terminates_sound … TERM EXEC');
    9991001            ##| ##skip
     
    10081010            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
    10091011            ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV;
    1010             napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
     1012            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR);
    10111013            napply (silent_sound … DIVERGING EXECDIV);
    10121014        ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS;
     
    10171019            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    10181020            #E7; nrewrite < E7 in REACTING; #REACTING;
    1019             napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
     1021            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL'');
    10201022            napply (reacts_sound … REACTING EXEC');
    10211023        ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG;
     
    10241026            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
    10251027            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
    1026             ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
     1028            ncut (e0 = e''); ##[ ndestruct (E6) skip (INITIAL MATCHES EXEC0 EXEC'); // ##]
    10271029            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
    10281030            nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL;
    1029             napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
     1031            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP);
    10301032            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
    10311033        ##| #E; ndestruct (E);
     
    10351037    #NOINIT; #_; #EXEC;
    10361038    @ (Goes_wrong E0); @;
    1037     ##[ nwhd in EXEC:(?(??%)?);
    1038         nrewrite > (exec_inf_aux_unfold …) in EXEC; nwhd in ⊢ (?%? → ?);
    1039         ncases e;
     1039    ##[ nwhd in EXEC:(?%?);
     1040        ncases e in EXEC;
    10401041        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
    10411042        ncases (se_inv … EXEC0);
    10421043        napply emb_initially_wrong;
    1043     ##| napply program_goes_initially_wrong;
    1044         #s; @; napply NOINIT;
    1045     ##]
    1046 ##] nqed.
    1047 
     1044    ##| #ge Ege;
     1045        napply program_goes_initially_wrong;
     1046        #s; @; #INIT; ncases (NOINIT s INIT); #ge' H; napply H;
     1047    ##]
     1048##] nqed.
     1049
Note: See TracChangeset for help on using the changeset viewer.