Revu la repartition des sources Coq en sous-repertoires

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

1 files changed, 0 insertions, 563 deletions

diff --git a/backend/Csharpminor.v b/backend/Csharpminor.v
deleted file mode 100644
index 246ebf53..00000000
--- a/backend/Csharpminor.v
+++ /dev/null
@@ -1,563 +0,0 @@
-(** Abstract syntax and semantics for the Csharpminor language. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Mem.
-Require Import Events.
-Require Import Globalenvs.
-
-(** Abstract syntax *)
-
-(** Csharpminor is a low-level imperative language structured in expressions,
-  statements, functions and programs.  Expressions include
-  reading global or local variables, reading store locations,
-  arithmetic operations, function calls, and conditional expressions
-  (similar to [e1 ? e2 : e3] in C).  The [Elet] and [Eletvar] constructs
-  enable sharing the computations of subexpressions.  De Bruijn notation
-  is used: [Eletvar n] refers to the value bound by then [n+1]-th enclosing
-  [Elet] construct.
-
-  Unlike in Cminor (the next intermediate language of the back-end),
-  Csharpminor local variables reside in memory, and their address can
-  be taken using [Eaddrof] expressions.
-
-  Another difference with Cminor is that Csharpminor is entirely 
-  processor-neutral. In particular, Csharpminor uses a standard set of
-  operations: it does not reflect processor-specific operations nor
-  addressing modes. *)
-
-Inductive operation : Set :=
-  | Ointconst: int -> operation         (**r integer constant *)
-  | Ofloatconst: float -> operation     (**r floating-point constant *)
-  | Ocast8unsigned: operation           (**r 8-bit zero extension  *)
-  | Ocast8signed: operation             (**r 8-bit sign extension  *)
-  | Ocast16unsigned: operation          (**r 16-bit zero extension  *)
-  | Ocast16signed: operation            (**r 16-bit sign extension *)
-  | Onotint: operation                  (**r bitwise complement  *)
-  | Oadd: operation                     (**r integer addition *)
-  | Osub: operation                     (**r integer subtraction *)
-  | Omul: operation                     (**r integer multiplication *)
-  | Odiv: operation                     (**r integer signed division *)
-  | Odivu: operation                    (**r integer unsigned division *)
-  | Omod: operation                     (**r integer signed modulus *)
-  | Omodu: operation                    (**r integer unsigned modulus *)
-  | Oand: operation                     (**r bitwise ``and'' *)
-  | Oor: operation                      (**r bitwise ``or'' *)
-  | Oxor: operation                     (**r bitwise ``xor'' *)
-  | Oshl: operation                     (**r left shift *)
-  | Oshr: operation                     (**r right signed shift *)
-  | Oshru: operation                    (**r right unsigned shift *)
-  | Onegf: operation                    (**r float opposite *)
-  | Oabsf: operation                    (**r float absolute value *)
-  | Oaddf: operation                    (**r float addition *)
-  | Osubf: operation                    (**r float subtraction *)
-  | Omulf: operation                    (**r float multiplication *)
-  | Odivf: operation                    (**r float division *)
-  | Osingleoffloat: operation           (**r float truncation *)
-  | Ointoffloat: operation              (**r integer to float *)
-  | Ofloatofint: operation              (**r float to signed integer *)
-  | Ofloatofintu: operation             (**r float to unsigned integer *)
-  | Ocmp: comparison -> operation       (**r integer signed comparison *)
-  | Ocmpu: comparison -> operation      (**r integer unsigned comparison *)
-  | Ocmpf: comparison -> operation.     (**r float comparison *)
-
-Inductive expr : Set :=
-  | Evar : ident -> expr                (**r reading a scalar variable  *)
-  | Eaddrof : ident -> expr             (**r taking the address of a variable *)
-  | Eop : operation -> exprlist -> expr (**r arithmetic operation *)
-  | Eload : memory_chunk -> expr -> expr (**r memory read *)
-  | Ecall : signature -> expr -> exprlist -> expr (**r function call *)
-  | Econdition : expr -> expr -> expr -> expr (**r conditional expression *)
-  | Elet : expr -> expr -> expr         (**r let binding  *)
-  | Eletvar : nat -> expr               (**r reference to a let-bound variable *)
-  | Ealloc : expr -> expr               (**r memory allocation *)
-
-with exprlist : Set :=
-  | Enil: exprlist
-  | Econs: expr -> exprlist -> exprlist.
-
-(** Statements include expression evaluation, variable assignment,
-  memory stores, an if/then/else conditional,
-  infinite loops, blocks and early block exits, and early function returns.
-  [Sexit n] terminates prematurely the execution of the [n+1] enclosing
-  [Sblock] statements. *)
-
-Inductive stmt : Set :=
-  | Sskip: stmt
-  | Sexpr: expr -> stmt
-  | Sassign : ident -> expr -> stmt
-  | Sstore : memory_chunk -> expr -> expr -> stmt
-  | Sseq: stmt -> stmt -> stmt
-  | Sifthenelse: expr -> stmt -> stmt -> stmt
-  | Sloop: stmt -> stmt
-  | Sblock: stmt -> stmt
-  | Sexit: nat -> stmt
-  | Sswitch: expr -> list (int * nat) -> nat -> stmt
-  | Sreturn: option expr -> stmt.
-
-(** The variables can be either scalar variables
-  (whose type, size and signedness are given by a [memory_chunk]
-  or array variables (of the indicated sizes).  The only operation
-  permitted on an array variable is taking its address. *)
-
-Inductive var_kind : Set :=
-  | Vscalar: memory_chunk -> var_kind
-  | Varray: Z -> var_kind.
-
-(** Functions are composed of a signature, a list of parameter names
-  with associated memory chunks (parameters must be scalar), a list of
-  local variables with associated [var_kind] description, and a
-  statement representing the function body.  *)
-
-Record function : Set := mkfunction {
-  fn_sig: signature;
-  fn_params: list (ident * memory_chunk);
-  fn_vars: list (ident * var_kind);
-  fn_body: stmt
-}.
-
-Definition fundef := AST.fundef function.
-
-Record program : Set := mkprogram {
-  prog_funct: list (ident * fundef);
-  prog_main: ident;
-  prog_vars: list (ident * var_kind * list init_data)
-}.
-
-Definition funsig (fd: fundef) :=
-  match fd with
-  | Internal f => f.(fn_sig)
-  | External ef => ef.(ef_sig)
-  end.
-
-(** * Operational semantics *)
-
-(** The operational semantics for Csharpminor is given in big-step operational
-  style.  Expressions evaluate to values, and statements evaluate to
-  ``outcomes'' indicating how execution should proceed afterwards. *)
-
-Inductive outcome: Set :=
-  | Out_normal: outcome                (**r continue in sequence *)
-  | Out_exit: nat -> outcome           (**r terminate [n+1] enclosing blocks *)
-  | Out_return: option val -> outcome. (**r return immediately to caller *)
-
-Definition outcome_result_value
-                 (out: outcome) (ot: option typ) (v: val) : Prop :=
-  match out, ot with
-  | Out_normal, None => v = Vundef
-  | Out_return None, None => v = Vundef
-  | Out_return (Some v'), Some ty => v = v'
-  | _, _ => False
-  end.
-
-Definition outcome_block (out: outcome) : outcome :=
-  match out with
-  | Out_normal => Out_normal
-  | Out_exit O => Out_normal
-  | Out_exit (S n) => Out_exit n
-  | Out_return optv => Out_return optv
-  end.
-
-Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat))
-                       {struct cases} : nat :=
-  match cases with
-  | nil => dfl
-  | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem
-  end.
-
-(** Four kinds of evaluation environments are involved:
-- [genv]: global environments, define symbols and functions;
-- [gvarenv]: map global variables to var info;
-- [env]: local environments, map local variables to memory blocks + var info;
-- [lenv]: let environments, map de Bruijn indices to values.
-*)
-Definition genv := Genv.t fundef.
-Definition gvarenv := PTree.t var_kind.
-Definition env := PTree.t (block * var_kind).
-Definition empty_env : env := PTree.empty (block * var_kind).
-Definition letenv := list val.
-
-Definition sizeof (lv: var_kind) : Z :=
-  match lv with
-  | Vscalar chunk => size_chunk chunk
-  | Varray sz => Zmax 0 sz
-  end.
-
-Definition program_of_program (p: program): AST.program fundef :=
-  AST.mkprogram
-    p.(prog_funct)
-    p.(prog_main)
-    (List.map (fun x => match x with (id, k, init) => (id, init) end) p.(prog_vars)).
-
-Definition fn_variables (f: function) :=
-  List.map
-    (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) f.(fn_params)
-  ++ f.(fn_vars).
-
-Definition fn_params_names (f: function) :=
-  List.map (@fst ident memory_chunk) f.(fn_params).
-
-Definition fn_vars_names (f: function) :=
-  List.map (@fst ident var_kind) f.(fn_vars).
-
-Definition global_var_env (p: program): gvarenv :=
-  List.fold_left
-    (fun gve x => match x with (id, k, init) => PTree.set id k gve end)
-    p.(prog_vars) (PTree.empty var_kind).
-
-(** Evaluation of operator applications. *)
-
-Definition eval_compare_null (c: comparison) (n: int) : option val :=
-  if Int.eq n Int.zero 
-  then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end
-  else None.
-
-Definition eval_operation (op: operation) (vl: list val) (m: mem): option val :=
-  match op, vl with
-  | Ointconst n, nil => Some (Vint n)
-  | Ofloatconst n, nil => Some (Vfloat n)
-  | Ocast8unsigned, Vint n1 :: nil => Some (Vint (Int.cast8unsigned n1))
-  | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1))
-  | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1))
-  | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1))
-  | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1))
-  | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2))
-  | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1))
-  | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2))
-  | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2))
-  | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2))
-  | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
-      if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None
-  | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2))
-  | Odiv, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2))
-  | Odivu, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
-  | Omod, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
-  | Omodu, Vint n1 :: Vint n2 :: nil =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
-  | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2))
-  | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2))
-  | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2))
-  | Oshl, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None
-  | Oshr, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
-  | Oshru, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
-  | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1))
-  | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1))
-  | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2))
-  | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2))
-  | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2))
-  | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2))
-  | Osingleoffloat, Vfloat f1 :: nil =>
-      Some (Vfloat (Float.singleoffloat f1))
-  | Ointoffloat, Vfloat f1 :: nil => 
-      Some (Vint (Float.intoffloat f1))
-  | Ofloatofint, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofint n1))
-  | Ofloatofintu, Vint n1 :: nil => 
-      Some (Vfloat (Float.floatofintu n1))
-  | Ocmp c, Vint n1 :: Vint n2 :: nil =>
-      Some (Val.of_bool(Int.cmp c n1 n2))
-  | Ocmp c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
-      if valid_pointer m b1 (Int.signed n1)
-      && valid_pointer m b2 (Int.signed n2) then
-        if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None
-      else
-        None
-  | Ocmp c, Vptr b1 n1 :: Vint n2 :: nil => eval_compare_null c n2
-  | Ocmp c, Vint n1 :: Vptr b2 n2 :: nil => eval_compare_null c n1
-  | Ocmpu c, Vint n1 :: Vint n2 :: nil =>
-      Some (Val.of_bool(Int.cmpu c n1 n2))
-  | Ocmpf c, Vfloat f1 :: Vfloat f2 :: nil =>
-      Some (Val.of_bool (Float.cmp c f1 f2))
-  | _, _ => None
-  end.
-
-(** Allocation of local variables at function entry.  Each variable is
-  bound to the reference to a fresh block of the appropriate size. *)
-
-Inductive alloc_variables: env -> mem ->
-                           list (ident * var_kind) ->
-                           env -> mem -> list block -> Prop :=
-  | alloc_variables_nil:
-      forall e m,
-      alloc_variables e m nil e m nil
-  | alloc_variables_cons:
-      forall e m id lv vars m1 b1 m2 e2 lb,
-      Mem.alloc m 0 (sizeof lv) = (m1, b1) ->
-      alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 lb ->
-      alloc_variables e m ((id, lv) :: vars) e2 m2 (b1 :: lb).
-
-(** Initialization of local variables that are parameters.  The value
-  of the corresponding argument is stored into the memory block
-  bound to the parameter. *)
-
-Inductive bind_parameters: env ->
-                           mem -> list (ident * memory_chunk) -> list val ->
-                           mem -> Prop :=
-  | bind_parameters_nil:
-      forall e m,
-      bind_parameters e m nil nil m
-  | bind_parameters_cons:
-      forall e m id chunk params v1 vl b m1 m2,
-      PTree.get id e = Some (b, Vscalar chunk) ->
-      Mem.store chunk m b 0 v1 = Some m1 ->
-      bind_parameters e m1 params vl m2 ->
-      bind_parameters e m ((id, chunk) :: params) (v1 :: vl) m2.
-
-Section RELSEM.
-
-Variable prg: program.
-Let ge := Genv.globalenv (program_of_program prg).
-
-(* Evaluation of the address of a variable: 
-   [eval_var_addr prg ge e id b] states that variable [id] 
-   in environment [e] evaluates to block [b]. *)
-
-Inductive eval_var_addr: env -> ident -> block -> Prop :=
-  | eval_var_addr_local:
-      forall e id b vi,
-      PTree.get id e = Some (b, vi) ->
-      eval_var_addr e id b
-  | eval_var_addr_global:
-      forall e id b,
-      PTree.get id e = None ->
-      Genv.find_symbol ge id = Some b ->
-      eval_var_addr e id b.
-
-(* Evaluation of a reference to a scalar variable:
-   [eval_var_ref prg ge e id b chunk] states
-   that variable [id] in environment [e] evaluates to block [b]
-   and is associated with the memory chunk [chunk]. *)
-
-Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop :=
-  | eval_var_ref_local:
-      forall e id b chunk,
-      PTree.get id e = Some (b, Vscalar chunk) ->
-      eval_var_ref e id b chunk
-  | eval_var_ref_global:
-      forall e id b chunk,
-      PTree.get id e = None ->
-      Genv.find_symbol ge id = Some b ->
-      PTree.get id (global_var_env prg) = Some (Vscalar chunk) ->
-      eval_var_ref e id b chunk.
-
-(** Evaluation of an expression: [eval_expr prg le e m a m' v] states
-  that expression [a], in initial memory state [m], evaluates to value
-  [v].  [m'] is the final memory state, respectively, reflecting
-  memory stores possibly performed by [a].  [e] and [le] are the
-  local environment and let environment respectively. *)
-
-Inductive eval_expr:
-         letenv -> env ->
-         mem -> expr -> trace -> mem -> val -> Prop :=
-  | eval_Evar:
-      forall le e m id b chunk v,
-      eval_var_ref e id b chunk ->
-      Mem.load chunk m b 0 = Some v ->
-      eval_expr le e m (Evar id) E0 m v
-  | eval_Eaddrof:
-      forall le e m id b,
-      eval_var_addr e id b ->
-      eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero)
-  | eval_Eop:
-      forall le e m op al t m1 vl v,
-      eval_exprlist le e m al t m1 vl ->
-      eval_operation op vl m1 = Some v ->
-      eval_expr le e m (Eop op al) t m1 v
-  | eval_Eload:
-      forall le e m chunk a t m1 v1 v,
-      eval_expr le e m a t m1 v1 ->
-      Mem.loadv chunk m1 v1 = Some v ->
-      eval_expr le e m (Eload chunk a) t m1 v
-  | eval_Ecall:
-      forall le e m sig a bl t1 m1 t2 m2 t3 m3 vf vargs vres f t,
-      eval_expr le e m a t1 m1 vf ->
-      eval_exprlist le e m1 bl t2 m2 vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall m2 f vargs t3 m3 vres ->
-      t = t1 ** t2 ** t3 ->
-      eval_expr le e m (Ecall sig a bl) t m3 vres
-  | eval_Econdition_true:
-      forall le e m a b c t1 m1 v1 t2 m2 v2 t,
-      eval_expr le e m a t1 m1 v1 ->
-      Val.is_true v1 ->
-      eval_expr le e m1 b t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr le e m (Econdition a b c) t m2 v2
-  | eval_Econdition_false:
-      forall le e m a b c t1 m1 v1 t2 m2 v2 t,
-      eval_expr le e m a t1 m1 v1 ->
-      Val.is_false v1 ->
-      eval_expr le e m1 c t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr le e m (Econdition a b c) t m2 v2
-  | eval_Elet:
-      forall le e m a b t1 m1 v1 t2 m2 v2 t,
-      eval_expr le e m a t1 m1 v1 ->
-      eval_expr (v1::le) e m1 b t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr le e m (Elet a b) t m2 v2
-  | eval_Eletvar:
-      forall le e m n v,
-      nth_error le n = Some v ->
-      eval_expr le e m (Eletvar n) E0 m v
-  | eval_Ealloc:
-      forall le e m a t m1 n m2 b,
-      eval_expr le e m a t m1 (Vint n) ->
-      Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
-      eval_expr le e m (Ealloc a) t m2 (Vptr b Int.zero)
-
-(** Evaluation of a list of expressions:
-  [eval_exprlist prg le al m a m' vl]
-  states that the list [al] of expressions evaluate 
-  to the list [vl] of values.
-  The other parameters are as in [eval_expr].
-*)
-
-with eval_exprlist:
-         letenv -> env ->
-         mem -> exprlist -> trace ->
-         mem -> list val -> Prop :=
-  | eval_Enil:
-      forall le e m,
-      eval_exprlist le e m Enil E0 m nil
-  | eval_Econs:
-      forall le e m a bl t1 m1 v t2 m2 vl t,
-      eval_expr le e m a t1 m1 v ->
-      eval_exprlist le e m1 bl t2 m2 vl ->
-      t = t1 ** t2 ->
-      eval_exprlist le e m (Econs a bl) t m2 (v :: vl)
-
-(** Evaluation of a function invocation: [eval_funcall prg m f args m' res]
-  means that the function [f], applied to the arguments [args] in
-  memory state [m], returns the value [res] in modified memory state [m'].
-*)
-with eval_funcall:
-        mem -> fundef -> list val -> trace ->
-        mem -> val -> Prop :=
-  | eval_funcall_internal:
-      forall m f vargs e m1 lb m2 t m3 out vres,
-      list_norepet (fn_params_names f ++ fn_vars_names f) ->
-      alloc_variables empty_env m (fn_variables f) e m1 lb ->
-      bind_parameters e m1 f.(fn_params) vargs m2 ->
-      exec_stmt e m2 f.(fn_body) t m3 out ->
-      outcome_result_value out f.(fn_sig).(sig_res) vres ->
-      eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres
-  | eval_funcall_external:
-      forall m ef vargs t vres,
-      event_match ef vargs t vres ->
-      eval_funcall m (External ef) vargs t m vres
-
-(** Execution of a statement: [exec_stmt prg e m s m' out]
-  means that statement [s] executes with outcome [out].
-  The other parameters are as in [eval_expr]. *)
-
-with exec_stmt:
-         env ->
-         mem -> stmt -> trace ->
-         mem -> outcome -> Prop :=
-  | exec_Sskip:
-      forall e m,
-      exec_stmt e m Sskip E0 m Out_normal
-  | exec_Sexpr:
-      forall e m a t m1 v,
-      eval_expr nil e m a t m1 v ->
-      exec_stmt e m (Sexpr a) t m1 Out_normal
-  | eval_Sassign:
-      forall e m id a t m1 b chunk v m2,
-      eval_expr nil e m a t m1 v ->
-      eval_var_ref e id b chunk ->
-      Mem.store chunk m1 b 0 v = Some m2 ->
-      exec_stmt e m (Sassign id a) t m2 Out_normal
-  | eval_Sstore:
-      forall e m chunk a b t1 m1 v1 t2 m2 v2 t3 m3,
-      eval_expr nil e m a t1 m1 v1 ->
-      eval_expr nil e m1 b t2 m2 v2 ->
-      Mem.storev chunk m2 v1 v2 = Some m3 ->
-      t3 = t1 ** t2 ->
-      exec_stmt e m (Sstore chunk a b) t3 m3 Out_normal
-  | exec_Sseq_continue:
-      forall e m s1 s2 t1 t2 m1 m2 t out,
-      exec_stmt e m s1 t1 m1 Out_normal ->
-      exec_stmt e m1 s2 t2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt e m (Sseq s1 s2) t m2 out
-  | exec_Sseq_stop:
-      forall e m s1 s2 t1 m1 out,
-      exec_stmt e m s1 t1 m1 out ->
-      out <> Out_normal ->
-      exec_stmt e m (Sseq s1 s2) t1 m1 out
-  | exec_Sifthenelse_true:
-      forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t,
-      eval_expr nil e m a t1 m1 v1 ->
-      Val.is_true v1 ->
-      exec_stmt e m1 sl1 t2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out
-  | exec_Sifthenelse_false:
-      forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t,
-      eval_expr nil e m a t1 m1 v1 ->
-      Val.is_false v1 ->
-      exec_stmt e m1 sl2 t2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out
-  | exec_Sloop_loop:
-      forall e m sl t1 m1 t2 m2 out t,
-      exec_stmt e m sl t1 m1 Out_normal ->
-      exec_stmt e m1 (Sloop sl) t2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt e m (Sloop sl) t m2 out
-  | exec_Sloop_stop:
-      forall e m sl t1 m1 out,
-      exec_stmt e m sl t1 m1 out ->
-      out <> Out_normal ->
-      exec_stmt e m (Sloop sl) t1 m1 out
-  | exec_Sblock:
-      forall e m sl t1 m1 out,
-      exec_stmt e m sl t1 m1 out ->
-      exec_stmt e m (Sblock sl) t1 m1 (outcome_block out)
-  | exec_Sexit:
-      forall e m n,
-      exec_stmt e m (Sexit n) E0 m (Out_exit n)
-  | exec_Sswitch:
-      forall e m a cases default t1 m1 n,
-      eval_expr nil e m a t1 m1 (Vint n) ->
-      exec_stmt e m (Sswitch a cases default)
-               t1 m1 (Out_exit (switch_target n default cases))
-  | exec_Sreturn_none:
-      forall e m,
-      exec_stmt e m (Sreturn None) E0 m (Out_return None)
-  | exec_Sreturn_some:
-      forall e m a t1 m1 v,
-      eval_expr nil e m a t1 m1 v ->
-      exec_stmt e m (Sreturn (Some a)) t1 m1 (Out_return (Some v)).
-
-Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop
-  with eval_exprlist_ind4 := Minimality for eval_exprlist Sort Prop
-  with eval_funcall_ind4 := Minimality for eval_funcall Sort Prop
-  with exec_stmt_ind4 := Minimality for exec_stmt Sort Prop.
-
-End RELSEM.
-
-(** Execution of a whole program: [exec_program p r]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] eventually returns value [r]. *)
-
-Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
-  let ge := Genv.globalenv (program_of_program p) in
-  let m0 := Genv.init_mem (program_of_program p) in
-  exists b, exists f, exists m,
-  Genv.find_symbol ge p.(prog_main) = Some b /\
-  Genv.find_funct_ptr ge b = Some f /\
-  funsig f = mksignature nil (Some Tint) /\
-  eval_funcall p m0 f nil t m r.