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

    r484 r485  
    9898#A B C P P' e f; nelim e; //;
    9999#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
    100 
    101 ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
    102 nlemma opt_OK: ∀A,P,e.
    103   (∀v. e = Some ? v → P v) →
    104   match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
    105 #A P e; nelim e; /2/;
    106 nqed.
    107100
    108101nlemma opt_bind_OK: ∀A,B,P,e,f.
     
    679672].
    680673
    681 nlet rec make_initial_state (p:clight_program) : res state
    682   let ge ≝ globalenv Genv ?? p in
    683   let m0 ≝ init_mem Genv ?? p in
    684     do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    685     do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
    686     do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    687     OK ? (Callstate f (nil ?) Kstop m0).
     674nlet rec make_initial_state (p:clight_program) : res (genv × state)
     675  do ge ← globalenv Genv ?? p;
     676  do m0 ← init_mem Genv ?? p;
     677  do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
     678  do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
     679  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     680  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
    688681
    689682ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
     
    756749
    757750ndefinition exec_inf : clight_program → execution ≝
    758 λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉).
     751λp.
     752  match make_initial_state p with
     753  [ OK gs ⇒ exec_inf_aux (\fst gs) (ret ? 〈E0,\snd gs〉)
     754  | _ ⇒ e_wrong
     755  ].
    759756
    760757nremark execution_cases: ∀e.
Note: See TracChangeset for help on using the changeset viewer.