Changeset 1231 for src/Clight/Csem.ma


Ignore:
Timestamp:
Sep 20, 2011, 7:11:41 PM (8 years ago)
Author:
campbell
Message:

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1147 r1231  
    12111211inductive initial_state (p: clight_program): state -> Prop :=
    12121212  | initial_state_intro: ∀b,f,ge,m0.
    1213       globalenv Genv ?? (fst ??) p = OK ? ge →
     1213      globalenv Genv ?? (fst ??) p = ge →
    12141214      init_mem Genv ?? (fst ??) p = OK ? m0 →
    12151215      find_symbol ?? ge (prog_main ?? p) = Some ? b →
     
    12291229
    12301230definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1231   ∀ge. globalenv ??? (fst ??) p = OK ? ge →
     1231  ∀ge. globalenv ??? (fst ??) p = ge →
    12321232  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    12331233 
Note: See TracChangeset for help on using the changeset viewer.