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

    r484 r485  
    14761476
    14771477ninductive initial_state (p: clight_program): state -> Prop :=
    1478   | initial_state_intro: ∀b,f.
    1479       let ge := globalenv Genv ?? p in
    1480       let m0 := init_mem Genv ?? p in
    1481       find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 ->
    1482       find_funct_ptr ?? ge b = Some ? f ->
     1478  | initial_state_intro: ∀b,f,ge,m0.
     1479      globalenv Genv ?? p = OK ? ge →
     1480      init_mem Genv ?? p = OK ? m0 →
     1481      find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉
     1482      find_funct_ptr ?? ge b = Some ? f
    14831483      initial_state p (Callstate f (nil ?) Kstop m0).
    14841484
     
    14951495
    14961496ndefinition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1497   program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
     1497  ∀ge. globalenv ??? p = OK ? ge →
     1498  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    14981499(*
    14991500(** Big-step execution of a whole program.  *)
Note: See TracChangeset for help on using the changeset viewer.