Changeset 1139 for src/Clight/Csem.ma
- Timestamp:
- Aug 30, 2011, 12:47:18 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csem.ma
r1058 r1139 1511 1511 inductive initial_state (p: clight_program): state -> Prop := 1512 1512 | 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 → 1515 1515 find_symbol ?? ge (prog_main ?? p) = Some ? b → 1516 1516 find_funct_ptr ?? ge b = Some ? f → … … 1529 1529 1530 1530 definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. 1531 ∀ge. globalenv ??? p = OK ? ge →1531 ∀ge. globalenv ??? (fst ??) p = OK ? ge → 1532 1532 program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. 1533 1533 (*
Note: See TracChangeset
for help on using the changeset viewer.