Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 3 insertions, 9 deletions

diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index d2eb3c1..c192e46 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -557,13 +557,7 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate (Vint r) Kstop m) r.
 
-(** Execution of a whole program: [exec_program p beh]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] has [beh] as observable
-  behavior. *)
-
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state 
-                  (Genv.globalenv p) beh.
-
+(** Wrapping up these definitions in a small-step semantics. *)
 
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).