Ignore:
Timestamp:
Feb 2, 2011, 12:41:05 PM (8 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/CexecSound.ma

    r484 r485  
    11include "Cexec.ma".
     2
     3include "Plogic/connectives.ma".
    24
    35nlemma exec_bool_of_val_sound: ∀v,ty,r.
     
    455457nqed.
    456458
    457 nlemma make_initial_state_sound : ∀p. P_res ? (λs.initial_state p s) (make_initial_state p).
     459nlemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
    458460#p; ncases p; #fns main vars;
    459461nwhd in ⊢ (???%);
     462napply bind_OK; #ge Ege;
     463napply bind_OK; #m Em;
    460464napply opt_bind_OK; #x; ncases x; #sp b esb;
    461465napply opt_bind_OK; #u ecode;
    462466napply opt_bind_OK; #f ef;
    463467ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
    464 nwhd; napply (initial_state_intro … esb ef);
     468nwhd; @; //; napply (initial_state_intro … Ege Em esb ef);
    465469nqed.
    466470
Note: See TracChangeset for help on using the changeset viewer.