Changeset 1139 for src/Clight/Csem.ma


Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (8 years ago)
Author:
campbell
Message:

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1058 r1139  
    15111511inductive initial_state (p: clight_program): state -> Prop :=
    15121512  | initial_state_intro: ∀b,f,ge,m0.
    1513       globalenv Genv ?? p = OK ? ge →
    1514       init_mem Genv ?? p = OK ? m0 →
     1513      globalenv Genv ?? (fst ??) p = OK ? ge →
     1514      init_mem Genv ?? (fst ??) p = OK ? m0 →
    15151515      find_symbol ?? ge (prog_main ?? p) = Some ? b →
    15161516      find_funct_ptr ?? ge b = Some ? f →
     
    15291529
    15301530definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1531   ∀ge. globalenv ??? p = OK ? ge →
     1531  ∀ge. globalenv ??? (fst ??) p = OK ? ge →
    15321532  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    15331533(*
Note: See TracChangeset for help on using the changeset viewer.