Merge of branches/full-expr-4:

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



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

1 files changed, 617 insertions, 1176 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 212c2add..2858e642 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -30,6 +30,67 @@ Require Import Smallstep.
 
 (** * Semantics of type-dependent operations *)
 
+(** Semantics of casts.  [cast v1 t1 t2 v2] holds if value [v1],
+  viewed with static type [t1], can be cast to type [t2],
+  resulting in value [v2].  *)
+
+Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
+  match sz, sg with
+  | I8, Signed => Int.sign_ext 8 i
+  | I8, Unsigned => Int.zero_ext 8 i
+  | I16, Signed => Int.sign_ext 16 i
+  | I16, Unsigned => Int.zero_ext 16 i 
+  | I32, _ => i
+  end.
+
+Definition cast_int_float (si : signedness) (i: int) : float :=
+  match si with
+  | Signed => Float.floatofint i
+  | Unsigned => Float.floatofintu i
+  end.
+
+Definition cast_float_int (si : signedness) (f: float) : int :=
+  match si with
+  | Signed => Float.intoffloat f
+  | Unsigned => Float.intuoffloat f
+  end.
+
+Definition cast_float_float (sz: floatsize) (f: float) : float :=
+  match sz with
+  | F32 => Float.singleoffloat f
+  | F64 => f
+  end.
+
+Inductive neutral_for_cast: type -> Prop :=
+  | nfc_int: forall sg,
+      neutral_for_cast (Tint I32 sg)
+  | nfc_ptr: forall ty,
+      neutral_for_cast (Tpointer ty)
+  | nfc_array: forall ty sz,
+      neutral_for_cast (Tarray ty sz)
+  | nfc_fun: forall targs tres,
+      neutral_for_cast (Tfunction targs tres).
+
+Inductive cast : val -> type -> type -> val -> Prop :=
+  | cast_ii:   forall i sz2 sz1 si1 si2,            (**r int to int  *)
+      cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
+           (Vint (cast_int_int sz2 si2 i))
+  | cast_fi:   forall f sz1 sz2 si2,                (**r float to int *)
+      cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
+           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
+  | cast_if:   forall i sz1 sz2 si1,                (**r int to float  *)
+      cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
+          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
+  | cast_ff:   forall f sz1 sz2,                    (**r float to float *)
+      cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)
+           (Vfloat (cast_float_float sz2 f))
+  | cast_nn_p: forall b ofs t1 t2, (**r no change in data representation *)
+      neutral_for_cast t1 -> neutral_for_cast t2 ->
+      cast (Vptr b ofs) t1 t2 (Vptr b ofs)
+  | cast_nn_i: forall n t1 t2,     (**r no change in data representation *)
+      neutral_for_cast t1 -> neutral_for_cast t2 ->
+      cast (Vint n) t1 t2 (Vint n).
+
 (** Interpretation of values as truth values.
   Non-zero integers, non-zero floats and non-null pointers are
   considered as true.  The integer zero (which also represents
@@ -59,6 +120,7 @@ Inductive is_true: val -> type -> Prop :=
       Float.cmp Ceq f Float.zero = false ->
       is_true (Vfloat f) (Tfloat sz).
 
+(*
 Inductive bool_of_val : val -> type -> val -> Prop :=
   | bool_of_val_true:   forall v ty, 
          is_true v ty -> 
@@ -66,67 +128,69 @@ Inductive bool_of_val : val -> type -> val -> Prop :=
   | bool_of_val_false:   forall v ty,
         is_false v ty ->
         bool_of_val v ty Vfalse.
+*)
 
 (** The following [sem_] functions compute the result of an operator
   application.  Since operators are overloaded, the result depends
   both on the static types of the arguments and on their run-time values.
-  Unlike in C, automatic conversions between integers and floats
-  are not performed.  For instance, [e1 + e2] is undefined if [e1]
-  is a float and [e2] an integer.  The Clight producer must have explicitly
-  promoted [e2] to a float. *)
+  For binary operations, the "usual binary conversions", adapted to a 32-bit
+  platform, state that:
+- If both arguments are of integer type, an integer operation is performed.
+  For operations that behave differently at unsigned and signed types
+  (e.g. division, modulus, comparisons), the unsigned operation is selected
+  if at least one of the arguments is of type "unsigned int 32", otherwise
+  the signed operation is performed.
+- If both arguments are of float type, a float operation is performed.
+  We choose to perform all float arithmetic in double precision,
+  even if both arguments are single-precision floats.
+- If one argument has integer type and the other has float type,
+  we convert the integer argument to float, then perform the float operation.
+ *)
 
 Function sem_neg (v: val) (ty: type) : option val :=
-  match ty with
-  | Tint _ _ =>
+  match classify_neg ty with
+  | neg_case_i sg =>
       match v with
       | Vint n => Some (Vint (Int.neg n))
       | _ => None
       end
-  | Tfloat _ =>
+  | neg_case_f =>
       match v with
       | Vfloat f => Some (Vfloat (Float.neg f))
       | _ => None
       end
-  | _ => None
-  end.
-
-Function sem_notint (v: val) : option val :=
-  match v with
-  | Vint n => Some (Vint (Int.xor n Int.mone))
-  | _ => None
+  | neg_default => None
   end.
 
-Function sem_notbool (v: val) (ty: type) : option val :=
-  match typeconv ty with
-  | Tint _ _ =>
+Function sem_notint (v: val) (ty: type): option val :=
+  match classify_notint ty with
+  | notint_case_i sg =>
       match v with
-      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
-      | Vptr _ _ => Some Vfalse
+      | Vint n => Some (Vint (Int.xor n Int.mone))
       | _ => None
       end
-  | Tpointer _ =>
+  | notint_default => None
+  end.
+
+Function sem_notbool (v: val) (ty: type) : option val :=
+  match classify_bool ty with
+  | bool_case_ip =>
       match v with
       | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
       | Vptr _ _ => Some Vfalse
       | _ => None
       end
-  | Tfloat _ =>
+  | bool_case_f =>
       match v with
       | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero))
       | _ => None
       end
-  | _ => None
-  end.
-
-Function sem_fabs (v: val) : option val :=
-  match v with
-  | Vfloat f => Some (Vfloat (Float.abs f))
-  | _ => None
+  | bool_default => None
   end.
 
 Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_add t1 t2 with 
-  | add_case_ii =>                      (**r integer addition *)
+  | add_case_ii sg =>                   (**r integer addition *)
       match v1, v2 with
       | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
       | _,  _ => None
@@ -136,6 +200,16 @@ Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2))
       | _,  _ => None
       end
+  | add_case_if sg =>                   (**r int plus float *)
+      match v1, v2 with
+      | Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2))
+      | _, _ => None
+      end
+  | add_case_fi sg =>                   (**r float plus int *)
+      match v1, v2 with
+      | Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2)))
+      | _, _ => None
+      end
   | add_case_pi ty =>                   (**r pointer plus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 => 
@@ -153,7 +227,7 @@ end.
 
 Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_sub t1 t2 with
-  | sub_case_ii =>               (**r integer subtraction *)
+  | sub_case_ii sg =>            (**r integer subtraction *)
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
       | _,  _ => None
@@ -163,6 +237,16 @@ Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2))
       | _,  _ => None
       end
+  | sub_case_if sg =>            (**r int minus float *)
+      match v1, v2 with
+      | Vint n1, Vfloat n2 => Some (Vfloat (Float.sub (cast_int_float sg n1) n2))
+      | _, _ => None
+      end
+  | sub_case_fi sg =>            (**r float minus int *)
+      match v1, v2 with
+      | Vfloat n1, Vint n2 => Some (Vfloat (Float.sub n1 (cast_int_float sg n2)))
+      | _, _ => None
+      end
   | sub_case_pi ty =>            (**r pointer minus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 => 
@@ -183,7 +267,7 @@ Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  
 Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_mul t1 t2 with
-  | mul_case_ii =>
+  | mul_case_ii sg =>
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2))
       | _,  _ => None
@@ -193,19 +277,29 @@ Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
       | _,  _ => None
       end
+  | mul_case_if sg =>
+      match v1, v2 with
+      | Vint n1, Vfloat n2 => Some (Vfloat (Float.mul (cast_int_float sg n1) n2))
+      | _, _ => None
+      end
+  | mul_case_fi sg =>
+      match v1, v2 with
+      | Vfloat n1, Vint n2 => Some (Vfloat (Float.mul n1 (cast_int_float sg n2)))
+      | _, _ => None
+      end
   | mul_default =>
       None
 end.
 
 Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
    match classify_div t1 t2 with
-  | div_case_I32unsi =>
+  | div_case_ii Unsigned =>
       match v1,v2 with
       | Vint n1, Vint n2 =>
           if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
       | _,_ => None
       end
-  | div_case_ii =>
+  | div_case_ii Signed =>
       match v1,v2 with
        | Vint n1, Vint n2 =>
           if Int.eq n2 Int.zero then None else Some (Vint(Int.divs n1 n2))
@@ -216,68 +310,94 @@ Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
       | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2))
       | _,  _ => None
       end 
+  | div_case_if sg =>
+      match v1, v2 with
+      | Vint n1, Vfloat n2 => Some (Vfloat (Float.div (cast_int_float sg n1) n2))
+      | _, _ => None
+      end
+  | div_case_fi sg =>
+      match v1, v2 with
+      | Vfloat n1, Vint n2 => Some (Vfloat (Float.div n1 (cast_int_float sg n2)))
+      | _, _ => None
+      end
   | div_default =>
       None
 end.
 
 Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_mod t1 t2 with
-  | mod_case_I32unsi =>
+  match classify_binint t1 t2 with
+  | binint_case_ii Unsigned =>
       match v1, v2 with
       | Vint n1, Vint n2 =>
           if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
       | _, _ => None
       end
-  | mod_case_ii =>
+  | binint_case_ii Signed =>
       match v1,v2 with
       | Vint n1, Vint n2 =>
           if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
       | _, _ => None
       end
-  | mod_default =>
+  | binint_default =>
       None
   end.
 
-Function sem_and (v1 v2: val) : option val :=
-  match v1, v2 with
-  | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2))
-  | _, _ => None
-  end .
-
-Function sem_or (v1 v2: val) : option val :=
-  match v1, v2 with
-  | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2))
-  | _, _ => None
-  end. 
-
-Function sem_xor (v1 v2: val): option val :=
-  match v1, v2 with
-  | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2))
-  | _, _ => None
+Function sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_binint t1 t2 with
+  | binint_case_ii sg =>
+      match v1, v2 with
+      | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2))
+      | _, _ => None
+      end
+  | binint_default => None
+  end.
+
+Function sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_binint t1 t2 with
+  | binint_case_ii sg =>
+      match v1, v2 with
+      | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2))
+      | _, _ => None
+      end
+  | binint_default => None
+  end.
+
+Function sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_binint t1 t2 with
+  | binint_case_ii sg =>
+      match v1, v2 with
+      | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2))
+      | _, _ => None
+      end
+  | binint_default => None
   end.
 
-Function sem_shl (v1 v2: val): option val :=
-  match v1, v2 with
-  | Vint n1, Vint n2 =>
-     if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None
-  | _, _ => None
+Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_shift t1 t2 with
+  | shift_case_ii sg =>
+      match v1, v2 with
+      | Vint n1, Vint n2 =>
+         if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None
+      | _, _ => None
+      end
+  | shift_default => None
   end.
 
 Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val :=
-  match classify_shr t1 t2 with 
-  | shr_case_I32unsi => 
+  match classify_shift t1 t2 with 
+  | shift_case_ii Unsigned =>
       match v1,v2 with 
       | Vint n1, Vint n2 =>
           if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
       | _,_ => None
       end
-   | shr_case_ii => 
+   | shift_case_ii Signed =>
       match v1,v2 with
       | Vint n1,  Vint n2 =>
           if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
       | _,  _ => None
       end
-   | shr_default=>
+   | shift_default =>
       None
    end.
 
@@ -292,7 +412,7 @@ Function sem_cmp (c:comparison)
                   (v1: val) (t1: type) (v2: val) (t2: type)
                   (m: mem): option val :=
   match classify_cmp t1 t2 with
-  | cmp_case_I32unsi =>
+  | cmp_case_iiu =>
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
       | _,  _ => None
@@ -318,6 +438,16 @@ Function sem_cmp (c:comparison)
       | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2))  
       | _,  _ => None
       end
+  | cmp_case_if sg =>
+      match v1, v2 with
+      | Vint n1, Vfloat n2 => Some (Val.of_bool (Float.cmp c (cast_int_float sg n1) n2))
+      | _, _ => None
+      end
+  | cmp_case_fi sg =>
+      match v1, v2 with
+      | Vfloat n1, Vint n2 => Some (Val.of_bool (Float.cmp c n1 (cast_int_float sg n2)))
+      | _, _ => None
+      end
   | cmp_default => None
   end.
 
@@ -325,9 +455,8 @@ Definition sem_unary_operation
             (op: unary_operation) (v: val) (ty: type): option val :=
   match op with
   | Onotbool => sem_notbool v ty
-  | Onotint => sem_notint v
+  | Onotint => sem_notint v ty
   | Oneg => sem_neg v ty
-  | Ofabs => sem_fabs v
   end.
 
 Definition sem_binary_operation
@@ -340,10 +469,10 @@ Definition sem_binary_operation
   | Omul => sem_mul v1 t1 v2 t2
   | Omod => sem_mod v1 t1 v2 t2
   | Odiv => sem_div v1 t1 v2 t2 
-  | Oand => sem_and v1 v2  
-  | Oor  => sem_or v1 v2 
-  | Oxor  => sem_xor v1 v2 
-  | Oshl => sem_shl v1 v2 
+  | Oand => sem_and v1 t1 v2 t2
+  | Oor  => sem_or v1 t1 v2 t2
+  | Oxor  => sem_xor v1 t1 v2 t2
+  | Oshl => sem_shl v1 t1 v2 t2
   | Oshr  => sem_shr v1 t1 v2 t2   
   | Oeq => sem_cmp Ceq v1 t1 v2 t2 m
   | One => sem_cmp Cne v1 t1 v2 t2 m
@@ -353,67 +482,12 @@ Definition sem_binary_operation
   | Oge => sem_cmp Cge v1 t1 v2 t2 m
   end.
 
-(** Semantic of casts.  [cast v1 t1 t2 v2] holds if value [v1],
-  viewed with static type [t1], can be cast to type [t2],
-  resulting in value [v2].  *)
-
-Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
-  match sz, sg with
-  | I8, Signed => Int.sign_ext 8 i
-  | I8, Unsigned => Int.zero_ext 8 i
-  | I16, Signed => Int.sign_ext 16 i
-  | I16, Unsigned => Int.zero_ext 16 i 
-  | I32, _ => i
-  end.
-
-Definition cast_int_float (si : signedness) (i: int) : float :=
-  match si with
-  | Signed => Float.floatofint i
-  | Unsigned => Float.floatofintu i
-  end.
-
-Definition cast_float_int (si : signedness) (f: float) : int :=
-  match si with
-  | Signed => Float.intoffloat f
-  | Unsigned => Float.intuoffloat f
-  end.
-
-Definition cast_float_float (sz: floatsize) (f: float) : float :=
-  match sz with
-  | F32 => Float.singleoffloat f
-  | F64 => f
+Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) :=
+  match id with
+  | Incr => sem_add v ty (Vint Int.one) (Tint I32 Signed)
+  | Decr => sem_sub v ty (Vint Int.one) (Tint I32 Signed)
   end.
 
-Inductive neutral_for_cast: type -> Prop :=
-  | nfc_int: forall sg,
-      neutral_for_cast (Tint I32 sg)
-  | nfc_ptr: forall ty,
-      neutral_for_cast (Tpointer ty)
-  | nfc_array: forall ty sz,
-      neutral_for_cast (Tarray ty sz)
-  | nfc_fun: forall targs tres,
-      neutral_for_cast (Tfunction targs tres).
-
-Inductive cast : val -> type -> type -> val -> Prop :=
-  | cast_ii:   forall i sz2 sz1 si1 si2,            (**r int to int  *)
-      cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
-           (Vint (cast_int_int sz2 si2 i))
-  | cast_fi:   forall f sz1 sz2 si2,                (**r float to int *)
-      cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
-           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
-  | cast_if:   forall i sz1 sz2 si1,                (**r int to float  *)
-      cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
-          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
-  | cast_ff:   forall f sz1 sz2,                    (**r float to float *)
-      cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)
-           (Vfloat (cast_float_float sz2 f))
-  | cast_nn_p: forall b ofs t1 t2, (**r no change in data representation *)
-      neutral_for_cast t1 -> neutral_for_cast t2 ->
-      cast (Vptr b ofs) t1 t2 (Vptr b ofs)
-  | cast_nn_i: forall n t1 t2,     (**r no change in data representation *)
-      neutral_for_cast t1 -> neutral_for_cast t2 ->
-      cast (Vint n) t1 t2 (Vint n).
-
 (** * Operational semantics *)
 
 (** The semantics uses two environments.  The global environment
@@ -422,7 +496,7 @@ Inductive cast : val -> type -> type -> val -> Prop :=
 
 Definition genv := Genv.t fundef type.
 
-(** The local environment maps local variables to block references.
+(** The local environment maps local variables to block references and types.
   The current value of the variable is stored in the associated memory
   block. *)
 
@@ -522,180 +596,328 @@ Section SEMANTICS.
 
 Variable ge: genv.
 
-(** ** Evaluation of expressions *)
+(** [type_of_global b] returns the type of the global variable or function
+  at address [b]. *)
+
+Definition type_of_global (b: block) : option type :=
+  match Genv.find_var_info ge b with
+  | Some gv => Some gv.(gvar_info)
+  | None =>
+      match Genv.find_funct_ptr ge b with
+      | Some fd => Some(type_of_fundef fd)
+      | None => None
+      end
+  end.
+
+(** ** Reduction semantics for expressions *)
 
 Section EXPR.
 
 Variable e: env.
-Variable m: mem.
-
-(** [eval_expr ge e m a v] defines the evaluation of expression [a]
-  in r-value position.  [v] is the value of the expression.
-  [e] is the current environment and [m] is the current memory state. *)
-
-Inductive eval_expr: expr -> val -> Prop :=
-  | eval_Econst_int:   forall i ty,
-      eval_expr (Expr (Econst_int i) ty) (Vint i)
-  | eval_Econst_float:   forall f ty,
-      eval_expr (Expr (Econst_float f) ty) (Vfloat f)
-  | eval_Elvalue: forall a ty loc ofs v,
-      eval_lvalue (Expr a ty) loc ofs ->
-      load_value_of_type ty m loc ofs = Some v ->
-      eval_expr (Expr a ty) v
-  | eval_Eaddrof: forall a ty loc ofs,
-      eval_lvalue a loc ofs ->
-      eval_expr (Expr (Eaddrof a) ty) (Vptr loc ofs)
-  | eval_Esizeof: forall ty' ty,
-      eval_expr (Expr (Esizeof ty') ty) (Vint (Int.repr (sizeof ty')))
-  | eval_Eunop:  forall op a ty v1 v,
-      eval_expr a v1 ->
-      sem_unary_operation op v1 (typeof a) = Some v ->
-      eval_expr (Expr (Eunop op a) ty) v
-  | eval_Ebinop: forall op a1 a2 ty v1 v2 v,
-      eval_expr a1 v1 ->
-      eval_expr a2 v2 ->
-      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
-      eval_expr (Expr (Ebinop op a1 a2) ty) v
-  | eval_Econdition_true: forall a1 a2 a3 ty v1 v2,
-      eval_expr a1 v1 ->
-      is_true v1 (typeof a1) ->
-      eval_expr a2 v2 ->
-      eval_expr (Expr (Econdition a1 a2 a3) ty) v2
-  | eval_Econdition_false: forall a1 a2 a3 ty v1 v3,
-      eval_expr a1 v1 ->
-      is_false v1 (typeof a1) ->
-      eval_expr a3 v3 ->
-      eval_expr (Expr (Econdition a1 a2 a3) ty) v3
-  | eval_Eorbool_1: forall a1 a2 ty v1,
-      eval_expr a1 v1 ->
-      is_true v1 (typeof a1) ->
-      eval_expr (Expr (Eorbool a1 a2) ty) Vtrue
-  | eval_Eorbool_2: forall a1 a2 ty v1 v2 v,
-      eval_expr a1 v1 ->
-      is_false v1 (typeof a1) -> 
-      eval_expr a2 v2 ->
-      bool_of_val v2 (typeof a2) v ->
-      eval_expr (Expr (Eorbool a1 a2) ty) v
-  | eval_Eandbool_1: forall a1 a2 ty v1,
-      eval_expr a1 v1 ->
-      is_false v1 (typeof a1) ->
-      eval_expr (Expr (Eandbool a1 a2) ty) Vfalse
-  | eval_Eandbool_2: forall a1 a2 ty v1 v2 v,
-      eval_expr a1 v1 ->
-      is_true v1 (typeof a1) -> 
-      eval_expr a2 v2 ->
-      bool_of_val v2 (typeof a2) v ->
-      eval_expr (Expr (Eandbool a1 a2) ty) v
-  | eval_Ecast:   forall a ty ty' v1 v,
-      eval_expr a v1 ->
-      cast v1 (typeof a) ty v ->
-      eval_expr (Expr (Ecast ty a) ty') v
-
-(** [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
-  in l-value position.  The result is the memory location [b, ofs]
-  that contains the value of the expression [a]. *)
-
-with eval_lvalue: expr -> block -> int -> Prop :=
-  | eval_Evar_local:   forall id l ty,
-      e!id = Some(l, ty) ->
-      eval_lvalue (Expr (Evar id) ty) l Int.zero
-  | eval_Evar_global: forall id l ty,
-      e!id = None ->
-      Genv.find_symbol ge id = Some l ->
-      eval_lvalue (Expr (Evar id) ty) l Int.zero
-  | eval_Ederef: forall a ty l ofs,
-      eval_expr a (Vptr l ofs) ->
-      eval_lvalue (Expr (Ederef a) ty) l ofs
- | eval_Efield_struct:   forall a i ty l ofs id fList delta,
-      eval_lvalue a l ofs ->
-      typeof a = Tstruct id fList ->
-      field_offset i fList = OK delta ->
-      eval_lvalue (Expr (Efield a i) ty) l (Int.add ofs (Int.repr delta))
- | eval_Efield_union:   forall a i ty l ofs id fList,
-      eval_lvalue a l ofs ->
-      typeof a = Tunion id fList ->
-      eval_lvalue (Expr (Efield a i) ty) l ofs.
-
-Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
-  with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop.
-
-(** [eval_exprlist ge e m al vl] evaluates a list of r-value
-  expressions [al] to their values [vl]. *)
-
-Inductive eval_exprlist: list expr -> list val -> Prop :=
-  | eval_Enil:
-      eval_exprlist nil nil
-  | eval_Econs:   forall a bl v vl,
-      eval_expr a v ->
-      eval_exprlist bl vl ->
-      eval_exprlist (a :: bl) (v :: vl).
-
-End EXPR.
-
-(** ** Transition semantics for statements and functions *)
-
-(** Continuations *)
+
+(** The semantics of expressions follows the popular Wright-Felleisen style.
+  It is a small-step semantics that reduces one redex at a time.
+  We first define head reductions (at the top of an expression, then
+  use reduction contexts to define reduction within an expression. *)
+
+(** Head reduction for l-values. *)
+
+Inductive lred: expr -> mem -> expr -> mem -> Prop :=
+  | red_var_local: forall x ty m b,
+      e!x = Some(b, ty) ->
+      lred (Evar x ty) m
+           (Eloc b Int.zero ty) m
+  | red_var_global: forall x ty m b,
+      e!x = None ->
+      Genv.find_symbol ge x = Some b ->
+      type_of_global b = Some ty ->
+      lred (Evar x ty) m
+           (Eloc b Int.zero ty) m
+  | red_deref: forall b ofs ty1 ty m,
+      lred (Ederef (Eval (Vptr b ofs) ty1) ty) m
+           (Eloc b ofs ty) m
+  | red_field_struct: forall b ofs id fList f ty m delta,
+      field_offset f fList = OK delta ->
+      lred (Efield (Eloc b ofs (Tstruct id fList)) f ty) m
+           (Eloc b (Int.add ofs (Int.repr delta)) ty) m
+  | red_field_union: forall b ofs id fList f ty m,
+      lred (Efield (Eloc b ofs (Tunion id fList)) f ty) m
+           (Eloc b ofs ty) m.
+
+(** Head reductions for r-values *)
+
+Inductive rred: expr -> mem -> expr -> mem -> Prop :=
+  | red_rvalof: forall b ofs ty m v,
+      load_value_of_type ty m b ofs = Some v ->
+      rred (Evalof (Eloc b ofs ty) ty) m
+           (Eval v ty) m
+  | red_addrof: forall b ofs ty1 ty m,
+      rred (Eaddrof (Eloc b ofs ty1) ty) m
+           (Eval (Vptr b ofs) ty) m
+  | red_unop: forall op v1 ty1 ty m v,
+      sem_unary_operation op v1 ty1 = Some v ->
+      rred (Eunop op (Eval v1 ty1) ty) m
+           (Eval v ty) m
+  | red_binop: forall op v1 ty1 v2 ty2 ty m v,
+      sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
+      rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m
+           (Eval v ty) m
+  | red_cast: forall ty v1 ty1 m v,
+      cast v1 ty1 ty v ->
+      rred (Ecast (Eval v1 ty1) ty) m
+           (Eval v ty) m
+  | red_condition_true: forall v1 ty1 r1 r2 ty m,
+      is_true v1 ty1 -> typeof r1 = ty ->
+      rred (Econdition (Eval v1 ty1) r1 r2 ty) m
+           (Eparen r1 ty) m
+  | red_condition_false: forall v1 ty1 r1 r2 ty m,
+      is_false v1 ty1 -> typeof r2 = ty ->
+      rred (Econdition (Eval v1 ty1) r1 r2 ty) m
+           (Eparen r2 ty) m
+  | red_sizeof: forall ty1 ty m,
+      rred (Esizeof ty1 ty) m
+           (Eval (Vint (Int.repr (sizeof ty1))) ty) m
+  | red_assign: forall b ofs ty1 v2 ty2 m v m',
+      cast v2 ty2 ty1 v ->
+      store_value_of_type ty1 m b ofs v = Some m' ->
+      rred (Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty1) m
+           (Eval v ty1) m'
+  | red_assignop: forall op b ofs ty1 v2 ty2 tyres m v1 v v' m',
+      load_value_of_type ty1 m b ofs = Some v1 ->
+      sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
+      cast v tyres ty1 v' ->
+      store_value_of_type ty1 m b ofs v' = Some m' ->
+      rred (Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty1) m
+           (Eval v' ty1) m'
+  | red_postincr: forall id b ofs ty m v1 v2 v3 m',
+      load_value_of_type ty m b ofs = Some v1 ->
+      sem_incrdecr id v1 ty = Some v2 ->
+      cast v2 (typeconv ty) ty v3 ->
+      store_value_of_type ty m b ofs v3 = Some m' ->
+      rred (Epostincr id (Eloc b ofs ty) ty) m
+           (Eval v1 ty) m'
+  | red_comma: forall v ty1 r2 ty m,
+      typeof r2 = ty ->
+      rred (Ecomma (Eval v ty1) r2 ty) m
+           r2 m
+  | red_paren: forall r ty m,
+      typeof r = ty ->
+      rred (Eparen r ty) m
+           r m.
+
+(** Head reduction for function calls.
+    (More exactly, identification of function calls that can reduce.) *)
+
+Inductive cast_arguments: exprlist -> typelist -> list val -> Prop :=
+  | cast_args_nil:
+      cast_arguments Enil Tnil nil
+  | cast_args_cons: forall v ty el targ1 targs v1 vl,
+      cast v ty targ1 v1 -> cast_arguments el targs vl ->
+      cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
+
+Inductive callred: expr -> fundef -> list val -> type -> Prop :=
+  | red_Ecall: forall vf tyargs tyres el ty fd vargs,
+      Genv.find_funct ge vf = Some fd ->
+      cast_arguments el tyargs vargs ->
+      type_of_fundef fd = Tfunction tyargs tyres ->
+      callred (Ecall (Eval vf (Tfunction tyargs tyres)) el ty)
+              fd vargs ty.
+
+(** Reduction contexts.  In accordance with C's nondeterministic semantics,
+  we allow reduction both to the left and to the right of a binary operator.
+  To enforce C's notion of sequence point, reductions within a conditional
+  [a ? b : c] can only take place in [a], not in [b] nor [c];
+  and reductions within a sequence [a, b] can only take place in [a], not in [b].
+
+  Reduction contexts are represented by functions [C] from expressions to expressions,
+  suitably constrained by the [context from to C] predicate below.
+  Contexts are "kinded" with respect to l-values and r-values:
+  [from] is the kind of the hole in the context and [to] is the kind of
+  the term resulting from filling the hole.
+*)
+
+Inductive kind : Type := LV | RV.
+
+Inductive context: kind -> kind -> (expr -> expr) -> Prop :=
+  | ctx_top: forall k,
+      context k k (fun x => x)
+  | ctx_deref: forall k C ty,
+      context k RV C -> context k LV (fun x => Ederef (C x) ty)
+  | ctx_field: forall k C f ty,
+      context k LV C -> context k LV (fun x => Efield (C x) f ty)
+  | ctx_rvalof: forall k C ty,
+      context k LV C -> context k RV (fun x => Evalof (C x) ty)
+  | ctx_addrof: forall k C ty,
+      context k LV C -> context k RV (fun x => Eaddrof (C x) ty)
+  | ctx_unop: forall k C op ty,
+      context k RV C -> context k RV (fun x => Eunop op (C x) ty)
+  | ctx_binop_left: forall k C op e2 ty,
+      context k RV C -> context k RV (fun x => Ebinop op (C x) e2 ty)
+  | ctx_binop_right: forall k C op e1 ty,
+      context k RV C -> context k RV (fun x => Ebinop op e1 (C x) ty)
+  | ctx_cast: forall k C ty,
+      context k RV C -> context k RV (fun x => Ecast (C x) ty)
+  | ctx_condition: forall k C r2 r3 ty,
+      context k RV C -> context k RV (fun x => Econdition (C x) r2 r3 ty)
+  | ctx_assign_left: forall k C e2 ty,
+      context k LV C -> context k RV (fun x => Eassign (C x) e2 ty)
+  | ctx_assign_right: forall k C e1 ty,
+      context k RV C -> context k RV (fun x => Eassign e1 (C x) ty)
+  | ctx_assignop_left: forall k C op e2 tyres ty,
+      context k LV C -> context k RV (fun x => Eassignop op (C x) e2 tyres ty)
+  | ctx_assignop_right: forall k C op e1 tyres ty,
+      context k RV C -> context k RV (fun x => Eassignop op e1 (C x) tyres ty)
+  | ctx_postincr: forall k C id ty,
+      context k LV C -> context k RV (fun x => Epostincr id (C x) ty)
+  | ctx_call_left: forall k C el ty,
+      context k RV C -> context k RV (fun x => Ecall (C x) el ty)
+  | ctx_call_right: forall k C e1 ty,
+      contextlist k C -> context k RV (fun x => Ecall e1 (C x) ty)
+  | ctx_comma: forall k C e2 ty,
+      context k RV C -> context k RV (fun x => Ecomma (C x) e2 ty)
+  | ctx_paren: forall k C ty,
+      context k RV C -> context k RV (fun x => Eparen (C x) ty)
+
+with contextlist: kind -> (expr -> exprlist) -> Prop :=
+  | ctx_list_head: forall k C el,
+      context k RV C -> contextlist k (fun x => Econs (C x) el)
+  | ctx_list_tail: forall k C e1,
+      contextlist k C -> contextlist k (fun x => Econs e1 (C x)).
+
+(** In a nondeterministic semantics, expressions can go wrong according
+  to one reduction order while being defined according to another.
+  Consider for instance [(x = 1) + (10 / x)] where [x] is initially [0].
+  This expression goes wrong if evaluated right-to-left, but is defined
+  if evaluated left-to-right.  Since our compiler is going to pick one
+  particular evaluation order, we must make sure that all orders are safe,
+  i.e. never evaluate a subexpression that goes wrong.
+
+  Being safe is a stronger requirement than just not getting stuck during
+  reductions.  Consider [f() + (10 / x)], where [f()] does not terminate.
+  This expression is never stuck because the evaluation of [f()] can make
+  infinitely many transitions.  Yet it contains a subexpression [10 / x]
+  that can go wrong if [x = 0], and the compiler may choose to evaluate
+  [10 / x] first, before calling [f()].  
+
+  Therefore, we must make sure that not only an expression cannot get stuck,
+  but none of its subexpressions can either.  We say that a subexpression
+  is not immediately stuck if it is a value (of the appropriate kind)
+  or it can reduce (at head or within). *)
+
+Inductive not_imm_stuck: kind -> expr -> mem -> Prop :=
+  | not_stuck_val: forall v ty m,
+      not_imm_stuck RV (Eval v ty) m
+  | not_stuck_loc: forall b ofs ty m,
+      not_imm_stuck LV (Eloc b ofs ty) m
+  | not_stuck_lred: forall to C e m e' m',
+      lred e m e' m' ->
+      context LV to C ->
+      not_imm_stuck to (C e) m
+  | not_stuck_rred: forall to C e m e' m',
+      rred e m e' m' ->
+      context RV to C ->
+      not_imm_stuck to (C e) m
+  | not_stuck_callred: forall to C e m fd args ty,
+      callred e fd args ty ->
+      context RV to C ->
+      not_imm_stuck to (C e) m.
+
+(* An expression is not stuck if none of the potential redexes contained within
+   is immediately stuck. *)
+
+Definition not_stuck (e: expr) (m: mem) : Prop :=
+  forall k C e' , 
+  context k RV C -> e = C e' -> not_imm_stuck k e' m.
+
+End EXPR. 
+
+(** ** Transition semantics. *)
+
+(** Continuations describe the computations that remain to be performed
+    after the statement or expression under consideration has
+    evaluated completely. *)
 
 Inductive cont: Type :=
   | Kstop: cont
-  | Kseq: statement -> cont -> cont
-       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
-  | Kwhile: expr -> statement -> cont -> cont
-       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
-  | Kdowhile: expr -> statement -> cont -> cont
-       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
-  | Kfor2: expr -> statement -> statement -> cont -> cont
-       (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
-  | Kfor3: expr -> statement -> statement -> cont -> cont
-       (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
-  | Kswitch: cont -> cont
-       (**r catches [break] statements arising out of [switch] *)
-  | Kcall: option (block * int * type) ->   (**r where to store result *)
-           function ->                      (**r calling function *)
-           env ->                           (**r local env of calling function *)
+  | Kdo: cont -> cont       (**r [Kdo k] = after [x] in [x;] *)
+  | Kseq: statement -> cont -> cont    (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
+  | Kifthenelse: statement -> statement -> cont -> cont     (**r [Kifthenelse s1 s2 k] = after [x] in [if (x) { s1 } else { s2 }] *)
+  | Kwhile1: expr -> statement -> cont -> cont      (**r [Kwhile1 x s k] = after [x] in [while(x) s] *)
+  | Kwhile2: expr -> statement -> cont -> cont      (**r [Kwhile x s k] = after [s] in [while (x) s] *)
+  | Kdowhile1: expr -> statement -> cont -> cont    (**r [Kdowhile1 x s k] = after [s] in [do s while (x)] *)
+  | Kdowhile2: expr -> statement -> cont -> cont    (**r [Kdowhile2 x s k] = after [x] in [do s while (x)] *)
+  | Kfor2: expr -> statement -> statement -> cont -> cont   (**r [Kfor2 e2 e3 s k] = after [e2] in [for(e1;e2;e3) s] *)
+  | Kfor3: expr -> statement -> statement -> cont -> cont   (**r [Kfor3 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
+  | Kfor4: expr -> statement -> statement -> cont -> cont   (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
+  | Kswitch1: labeled_statements -> cont -> cont     (**r [Kswitch1 ls k] = after [e] in [switch(e) { ls }] *)
+  | Kswitch2: cont -> cont       (**r catches [break] statements arising out of [switch] *)
+  | Kreturn: cont -> cont        (**r [Kreturn k] = after [e] in [return e;] *)
+  | Kcall: function ->           (**r calling function *)
+           env ->                (**r local env of calling function *)
+           (expr -> expr) ->     (**r context of the call *)
+           type ->               (**r type of call expression *)
            cont -> cont.
 
 (** Pop continuation until a call or stop *)
 
 Fixpoint call_cont (k: cont) : cont :=
   match k with
+  | Kstop => k
+  | Kdo k => k
   | Kseq s k => call_cont k
-  | Kwhile e s k => call_cont k
-  | Kdowhile e s k => call_cont k
+  | Kifthenelse s1 s2 k => call_cont k
+  | Kwhile1 e s k => call_cont k
+  | Kwhile2 e s k => call_cont k
+  | Kdowhile1 e s k => call_cont k
+  | Kdowhile2 e s k => call_cont k
   | Kfor2 e2 e3 s k => call_cont k
   | Kfor3 e2 e3 s k => call_cont k
-  | Kswitch k => call_cont k
-  | _ => k
+  | Kfor4 e2 e3 s k => call_cont k
+  | Kswitch1 ls k => call_cont k
+  | Kswitch2 k => call_cont k
+  | Kreturn k => call_cont k
+  | Kcall _ _ _ _ _ => k
   end.
 
 Definition is_call_cont (k: cont) : Prop :=
   match k with
   | Kstop => True
-  | Kcall _ _ _ _ => True
+  | Kcall _ _ _ _ _ => True
   | _ => False
   end.
 
-(** States *)
+(** Execution states of the program are grouped in 4 classes corresponding
+  to the part of the program we are currently executing.  It can be
+  a statement ([State]), an expression ([ExprState]), a transition
+  from a calling function to a called function ([Callstate]), or
+  the symmetrical transition from a function back to its caller
+  ([Returnstate]). *)
 
 Inductive state: Type :=
-  | State
+  | State                               (**r execution of a statement *)
       (f: function)
       (s: statement)
       (k: cont)
       (e: env)
       (m: mem) : state
-  | Callstate
+  | ExprState                           (**r reduction of an expression *)
+      (f: function)
+      (r: expr)
+      (k: cont)
+      (e: env)
+      (m: mem) : state
+  | Callstate                           (**r calling a function *)
       (fd: fundef)
       (args: list val)
       (k: cont)
       (m: mem) : state
-  | Returnstate
+  | Returnstate                         (**r returning from a function *)
       (res: val)
       (k: cont)
       (m: mem) : state.
                  
 (** Find the statement and manufacture the continuation 
-  corresponding to a label *)
+  corresponding to a label. *)
 
 Fixpoint find_label (lbl: label) (s: statement) (k: cont) 
                     {struct s}: option (statement * cont) :=
@@ -711,20 +933,20 @@ Fixpoint find_label (lbl: label) (s: statement) (k: cont)
       | None => find_label lbl s2 k
       end
   | Swhile a s1 =>
-      find_label lbl s1 (Kwhile a s1 k)
+      find_label lbl s1 (Kwhile2 a s1 k)
   | Sdowhile a s1 =>
-      find_label lbl s1 (Kdowhile a s1 k)
+      find_label lbl s1 (Kdowhile1 a s1 k)
   | Sfor a1 a2 a3 s1 =>
       match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with
       | Some sk => Some sk
       | None =>
-          match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
+          match find_label lbl s1 (Kfor3 a2 a3 s1 k) with
           | Some sk => Some sk
-          | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
+          | None => find_label lbl a3 (Kfor4 a2 a3 s1 k)
           end
       end
   | Sswitch e sl =>
-      find_label_ls lbl sl (Kswitch k)
+      find_label_ls lbl sl (Kswitch2 k)
   | Slabel lbl' s' =>
       if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
   | _ => None
@@ -741,481 +963,196 @@ with find_label_ls (lbl: label) (sl: labeled_statements) (k: cont)
       end
   end.
 
-(** Transition relation *)
-
-Inductive step: state -> trace -> state -> Prop :=
-
-  | step_assign:   forall f a1 a2 k e m loc ofs v2 m',
-      eval_lvalue e m a1 loc ofs ->
-      eval_expr e m a2 v2 ->
-      store_value_of_type (typeof a1) m loc ofs v2 = Some m' ->
-      step (State f (Sassign a1 a2) k e m)
-        E0 (State f Sskip k e m')
-
-  | step_call_none:   forall f a al k e m vf vargs fd,
-      eval_expr e m a vf ->
-      eval_exprlist e m al vargs ->
-      Genv.find_funct ge vf = Some fd ->
-      type_of_fundef fd = typeof a ->
-      step (State f (Scall None a al) k e m)
-        E0 (Callstate fd vargs (Kcall None f e k) m)
-
-  | step_call_some:   forall f lhs a al k e m loc ofs vf vargs fd,
-      eval_lvalue e m lhs loc ofs ->
-      eval_expr e m a vf ->
-      eval_exprlist e m al vargs ->
-      Genv.find_funct ge vf = Some fd ->
-      type_of_fundef fd = typeof a ->
-      step (State f (Scall (Some lhs) a al) k e m)
-        E0 (Callstate fd vargs (Kcall (Some(loc, ofs, typeof lhs)) f e k) m)
+(** We separate the transition rules in two groups:
+- one group that deals with reductions over expressions;
+- the other group that deals with everything else: statements, function calls, etc.
+
+This makes it easy to express different reduction strategies for expressions:
+the second group of rules can be reused as is. *)
+
+Inductive estep: state -> trace -> state -> Prop :=
+
+  | step_lred: forall C f a k e m a' m',
+      lred e a m a' m' ->
+      not_stuck e (C a) m ->
+      context LV RV C ->
+      estep (ExprState f (C a) k e m)
+         E0 (ExprState f (C a') k e m')
+
+  | step_rred: forall C f a k e m a' m',
+      rred a m a' m' ->
+      not_stuck e (C a) m ->
+      context RV RV C ->
+      estep (ExprState f (C a) k e m)
+         E0 (ExprState f (C a') k e m')
+
+  | step_call: forall C f a k e m fd vargs ty,
+      callred a fd vargs ty ->
+      not_stuck e (C a) m ->
+      context RV RV C ->
+      estep (ExprState f (C a) k e m)
+         E0 (Callstate fd vargs (Kcall f e C ty k) m).
+
+Inductive sstep: state -> trace -> state -> Prop :=
+
+  | step_do_1: forall f x k e m,
+      sstep (State f (Sdo x) k e m)
+        E0 (ExprState f x (Kdo k) e m)
+  | step_do_2: forall f v ty k e m,
+      sstep (ExprState f (Eval v ty) (Kdo k) e m)
+        E0 (State f Sskip k e m)
 
   | step_seq:  forall f s1 s2 k e m,
-      step (State f (Ssequence s1 s2) k e m)
+      sstep (State f (Ssequence s1 s2) k e m)
         E0 (State f s1 (Kseq s2 k) e m)
   | step_skip_seq: forall f s k e m,
-      step (State f Sskip (Kseq s k) e m)
+      sstep (State f Sskip (Kseq s k) e m)
         E0 (State f s k e m)
   | step_continue_seq: forall f s k e m,
-      step (State f Scontinue (Kseq s k) e m)
+      sstep (State f Scontinue (Kseq s k) e m)
         E0 (State f Scontinue k e m)
   | step_break_seq: forall f s k e m,
-      step (State f Sbreak (Kseq s k) e m)
+      sstep (State f Sbreak (Kseq s k) e m)
         E0 (State f Sbreak k e m)
 
-  | step_ifthenelse_true:  forall f a s1 s2 k e m v1,
-      eval_expr e m a v1 ->
-      is_true v1 (typeof a) ->
-      step (State f (Sifthenelse a s1 s2) k e m)
+  | step_ifthenelse: forall f a s1 s2 k e m,
+      sstep (State f (Sifthenelse a s1 s2) k e m)
+        E0 (ExprState f a (Kifthenelse s1 s2 k) e m)
+  | step_ifthenelse_true:  forall f v ty s1 s2 k e m,
+      is_true v ty ->
+      sstep (ExprState f (Eval v ty) (Kifthenelse s1 s2 k) e m)
         E0 (State f s1 k e m)
-  | step_ifthenelse_false: forall f a s1 s2 k e m v1,
-      eval_expr e m a v1 ->
-      is_false v1 (typeof a) ->
-      step (State f (Sifthenelse a s1 s2) k e m)
+  | step_ifthenelse_false: forall f v ty s1 s2 k e m,
+      is_false v ty ->
+      sstep (ExprState f (Eval v ty) (Kifthenelse s1 s2 k) e m)
         E0 (State f s2 k e m)
 
-  | step_while_false: forall f a s k e m v,
-      eval_expr e m a v ->
-      is_false v (typeof a) ->
-      step (State f (Swhile a s) k e m)
+  | step_while: forall f x s k e m,
+      sstep (State f (Swhile x s) k e m)
+        E0 (ExprState f x (Kwhile1 x s k) e m)
+  | step_while_false: forall f v ty x s k e m,
+      is_false v ty ->
+      sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m)
         E0 (State f Sskip k e m)
-  | step_while_true: forall f a s k e m v,
-      eval_expr e m a v ->
-      is_true v (typeof a) ->
-      step (State f (Swhile a s) k e m)
-        E0 (State f s (Kwhile a s k) e m)
-  | step_skip_or_continue_while: forall f x a s k e m,
-      x = Sskip \/ x = Scontinue ->
-      step (State f x (Kwhile a s k) e m)
-        E0 (State f (Swhile a s) k e m)
-  | step_break_while: forall f a s k e m,
-      step (State f Sbreak (Kwhile a s k) e m)
+  | step_while_true: forall f v ty x s k e m ,
+      is_true v ty ->
+      sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m)
+        E0 (State f s (Kwhile2 x s k) e m)
+  | step_skip_or_continue_while: forall f s0 x s k e m,
+      s0 = Sskip \/ s0 = Scontinue ->
+      sstep (State f s0 (Kwhile2 x s k) e m)
+        E0 (State f (Swhile x s) k e m)
+  | step_break_while: forall f x s k e m,
+      sstep (State f Sbreak (Kwhile2 x s k) e m)
         E0 (State f Sskip k e m)
 
   | step_dowhile: forall f a s k e m,
-      step (State f (Sdowhile a s) k e m)
-        E0 (State f s (Kdowhile a s k) e m)
-  | step_skip_or_continue_dowhile_false: forall f x a s k e m v,
-      x = Sskip \/ x = Scontinue ->
-      eval_expr e m a v ->
-      is_false v (typeof a) ->
-      step (State f x (Kdowhile a s k) e m)
+      sstep (State f (Sdowhile a s) k e m)
+        E0 (State f s (Kdowhile1 a s k) e m)
+  | step_skip_or_continue_dowhile: forall f s0 x s k e m,
+      s0 = Sskip \/ s0 = Scontinue ->
+      sstep (State f s0 (Kdowhile1 x s k) e m)
+        E0 (ExprState f x (Kdowhile2 x s k) e m)
+  | step_dowhile_false: forall f v ty x s k e m,
+      is_false v ty ->
+      sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m)
         E0 (State f Sskip k e m)
-  | step_skip_or_continue_dowhile_true: forall f x a s k e m v,
-      x = Sskip \/ x = Scontinue ->
-      eval_expr e m a v ->
-      is_true v (typeof a) ->
-      step (State f x (Kdowhile a s k) e m)
-        E0 (State f (Sdowhile a s) k e m)
+  | step_dowhile_true: forall f v ty x s k e m,
+      is_true v ty ->
+      sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m)
+        E0 (State f (Sdowhile x s) k e m)
   | step_break_dowhile: forall f a s k e m,
-      step (State f Sbreak (Kdowhile a s k) e m)
+      sstep (State f Sbreak (Kdowhile1 a s k) e m)
         E0 (State f Sskip k e m)
 
   | step_for_start: forall f a1 a2 a3 s k e m,
       a1 <> Sskip ->
-      step (State f (Sfor a1 a2 a3 s) k e m)
+      sstep (State f (Sfor a1 a2 a3 s) k e m)
         E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
-  | step_for_false: forall f a2 a3 s k e m v,
-      eval_expr e m a2 v ->
-      is_false v (typeof a2) ->
-      step (State f (Sfor Sskip a2 a3 s) k e m)
+  | step_for: forall f a2 a3 s k e m,
+      sstep (State f (Sfor Sskip a2 a3 s) k e m)
+        E0 (ExprState f a2 (Kfor2 a2 a3 s k) e m)
+  | step_for_false: forall f v ty a2 a3 s k e m,
+      is_false v ty ->
+      sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m)
         E0 (State f Sskip k e m)
-  | step_for_true: forall f a2 a3 s k e m v,
-      eval_expr e m a2 v ->
-      is_true v (typeof a2) ->
-      step (State f (Sfor Sskip a2 a3 s) k e m)
-        E0 (State f s (Kfor2 a2 a3 s k) e m)
-  | step_skip_or_continue_for2: forall f x a2 a3 s k e m,
+  | step_for_true: forall f v ty a2 a3 s k e m,
+      is_true v ty ->
+      sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m)
+        E0 (State f s (Kfor3 a2 a3 s k) e m)
+  | step_skip_or_continue_for3: forall f x a2 a3 s k e m,
       x = Sskip \/ x = Scontinue ->
-      step (State f x (Kfor2 a2 a3 s k) e m)
-        E0 (State f a3 (Kfor3 a2 a3 s k) e m)
-  | step_break_for2: forall f a2 a3 s k e m,
-      step (State f Sbreak (Kfor2 a2 a3 s k) e m)
+      sstep (State f x (Kfor3 a2 a3 s k) e m)
+        E0 (State f a3 (Kfor4 a2 a3 s k) e m)
+  | step_break_for3: forall f a2 a3 s k e m,
+      sstep (State f Sbreak (Kfor3 a2 a3 s k) e m)
         E0 (State f Sskip k e m)
-  | step_skip_for3: forall f a2 a3 s k e m,
-      step (State f Sskip (Kfor3 a2 a3 s k) e m)
+  | step_skip_for4: forall f a2 a3 s k e m,
+      sstep (State f Sskip (Kfor4 a2 a3 s k) e m)
         E0 (State f (Sfor Sskip a2 a3 s) k e m)
 
   | step_return_0: forall f k e m m',
       f.(fn_return) = Tvoid ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
-      step (State f (Sreturn None) k e m)
+      sstep (State f (Sreturn None) k e m)
         E0 (Returnstate Vundef (call_cont k) m')
-  | step_return_1: forall f a k e m v m',
+  | step_return_1: forall f x k e m,
       f.(fn_return) <> Tvoid ->
-      eval_expr e m a v ->
+      sstep (State f (Sreturn (Some x)) k e m)
+        E0 (ExprState f x (Kreturn k) e  m)
+  | step_return_2:  forall f v1 ty k e m v2 m',
+      cast v1 ty f.(fn_return) v2 ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
-      step (State f (Sreturn (Some a)) k e m)
-        E0 (Returnstate v (call_cont k) m')
+      sstep (ExprState f (Eval v1 ty) (Kreturn k) e m)
+        E0 (Returnstate v2 (call_cont k) m')
   | step_skip_call: forall f k e m m',
       is_call_cont k ->
       f.(fn_return) = Tvoid ->
       Mem.free_list m (blocks_of_env e) = Some m' ->
-      step (State f Sskip k e m)
+      sstep (State f Sskip k e m)
         E0 (Returnstate Vundef k m')
 
-  | step_switch: forall f a sl k e m n,
-      eval_expr e m a (Vint n) ->
-      step (State f (Sswitch a sl) k e m)
-        E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
+  | step_switch: forall f x sl k e m,
+      sstep (State f (Sswitch x sl) k e m)
+        E0 (ExprState f x (Kswitch1 sl k) e m)
+  | step_expr_switch: forall f n ty sl k e m,
+      sstep (ExprState f (Eval (Vint n) ty) (Kswitch1 sl k) e m)
+        E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
   | step_skip_break_switch: forall f x k e m,
       x = Sskip \/ x = Sbreak ->
-      step (State f x (Kswitch k) e m)
+      sstep (State f x (Kswitch2 k) e m)
         E0 (State f Sskip k e m)
   | step_continue_switch: forall f k e m,
-      step (State f Scontinue (Kswitch k) e m)
+      sstep (State f Scontinue (Kswitch2 k) e m)
         E0 (State f Scontinue k e m)
 
   | step_label: forall f lbl s k e m,
-      step (State f (Slabel lbl s) k e m)
+      sstep (State f (Slabel lbl s) k e m)
         E0 (State f s k e m)
 
   | step_goto: forall f lbl k e m s' k',
       find_label lbl f.(fn_body) (call_cont k) = Some (s', k') ->
-      step (State f (Sgoto lbl) k e m)
+      sstep (State f (Sgoto lbl) k e m)
         E0 (State f s' k' e m)
 
   | step_internal_function: forall f vargs k m e m1 m2,
+      list_norepet (var_names (fn_params f) ++ var_names (fn_vars f)) ->
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       bind_parameters e m1 f.(fn_params) vargs m2 ->
-      step (Callstate (Internal f) vargs k m)
+      sstep (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k e m2)
 
   | step_external_function: forall ef targs tres vargs k m vres t m',
       external_call ef  ge vargs m t vres m' ->
-      step (Callstate (External ef targs tres) vargs k m)
+      sstep (Callstate (External ef targs tres) vargs k m)
          t (Returnstate vres k m')
 
-  | step_returnstate_0: forall v f e k m,
-      step (Returnstate v (Kcall None f e k) m)
-        E0 (State f Sskip k e m)
-
-  | step_returnstate_1: forall v f e k m m' loc ofs ty,
-      store_value_of_type ty m loc ofs v = Some m' ->
-      step (Returnstate v (Kcall (Some(loc, ofs, ty)) f e k) m)
-        E0 (State f Sskip k e m').
-
-(** * Alternate big-step semantics *)
-
-(** ** Big-step semantics for terminating statements and functions *)
+  | step_returnstate: forall v f e C ty k m,
+      sstep (Returnstate v (Kcall f e C ty k) m)
+        E0 (ExprState f (C (Eval v ty)) k e m).
 
-(** The execution of a statement produces an ``outcome'', indicating
-  how the execution terminated: either normally or prematurely
-  through the execution of a [break], [continue] or [return] statement. *)
-
-Inductive outcome: Type :=
-   | Out_break: outcome                 (**r terminated by [break] *)
-   | Out_continue: outcome              (**r terminated by [continue] *)
-   | Out_normal: outcome                (**r terminated normally *)
-   | Out_return: option val -> outcome. (**r terminated by [return] *)
-
-Inductive out_normal_or_continue : outcome -> Prop :=
-  | Out_normal_or_continue_N: out_normal_or_continue Out_normal
-  | Out_normal_or_continue_C: out_normal_or_continue Out_continue.
-
-Inductive out_break_or_return : outcome -> outcome -> Prop :=
-  | Out_break_or_return_B: out_break_or_return Out_break Out_normal
-  | Out_break_or_return_R: forall ov,
-      out_break_or_return (Out_return ov) (Out_return ov).
-
-Definition outcome_switch (out: outcome) : outcome :=
-  match out with
-  | Out_break => Out_normal
-  | o => o
-  end.
-
-Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
-  match out, t with
-  | Out_normal, Tvoid => v = Vundef
-  | Out_return None, Tvoid => v = Vundef
-  | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v
-  | _, _ => False
-  end. 
-
-(** [exec_stmt ge e m1 s t m2 out] describes the execution of 
-  the statement [s].  [out] is the outcome for this execution.
-  [m1] is the initial memory state, [m2] the final memory state.
-  [t] is the trace of input/output events performed during this
-  evaluation. *)
-
-Inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
-  | exec_Sskip:   forall e m,
-      exec_stmt e m Sskip
-               E0 m Out_normal
-  | exec_Sassign:   forall e m a1 a2 loc ofs v2 m',
-      eval_lvalue e m a1 loc ofs ->
-      eval_expr e m a2 v2 ->
-      store_value_of_type (typeof a1) m loc ofs v2 = Some m' ->
-      exec_stmt e m (Sassign a1 a2)
-               E0 m' Out_normal
-  | exec_Scall_none:   forall e m a al vf vargs f t m' vres,
-      eval_expr e m a vf ->
-      eval_exprlist e m al vargs ->
-      Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
-      eval_funcall m f vargs t m' vres ->
-      exec_stmt e m (Scall None a al)
-                t m' Out_normal
-  | exec_Scall_some:   forall e m lhs a al loc ofs vf vargs f t m' vres m'',
-      eval_lvalue e m lhs loc ofs ->
-      eval_expr e m a vf ->
-      eval_exprlist e m al vargs ->
-      Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
-      eval_funcall m f vargs t m' vres ->
-      store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' ->
-      exec_stmt e m (Scall (Some lhs) a al)
-                t m'' Out_normal
-  | exec_Sseq_1:   forall e m s1 s2 t1 m1 t2 m2 out,
-      exec_stmt e m s1 t1 m1 Out_normal ->
-      exec_stmt e m1 s2 t2 m2 out ->
-      exec_stmt e m (Ssequence s1 s2)
-                (t1 ** t2) m2 out
-  | exec_Sseq_2:   forall e m s1 s2 t1 m1 out,
-      exec_stmt e m s1 t1 m1 out ->
-      out <> Out_normal ->
-      exec_stmt e m (Ssequence s1 s2)
-                t1 m1 out
-  | exec_Sifthenelse_true: forall e m a s1 s2 v1 t m' out,
-      eval_expr e m a v1 ->
-      is_true v1 (typeof a) ->
-      exec_stmt e m s1 t m' out ->
-      exec_stmt e m (Sifthenelse a s1 s2)
-                t m' out
-  | exec_Sifthenelse_false: forall e m a s1 s2 v1 t m' out,
-      eval_expr e m a v1 ->
-      is_false v1 (typeof a) ->
-      exec_stmt e m s2 t m' out ->
-      exec_stmt e m (Sifthenelse a s1 s2)
-                t m' out
-  | exec_Sreturn_none:   forall e m,
-      exec_stmt e m (Sreturn None)
-               E0 m (Out_return None)
-  | exec_Sreturn_some: forall e m a v,
-      eval_expr e m a v ->
-      exec_stmt e m (Sreturn (Some a))
-               E0 m (Out_return (Some v))
-  | exec_Sbreak:   forall e m,
-      exec_stmt e m Sbreak
-               E0 m Out_break
-  | exec_Scontinue:   forall e m,
-      exec_stmt e m Scontinue
-               E0 m Out_continue
-  | exec_Swhile_false: forall e m a s v,
-      eval_expr e m a v ->
-      is_false v (typeof a) ->
-      exec_stmt e m (Swhile a s)
-               E0 m Out_normal
-  | exec_Swhile_stop: forall e m a v s t m' out' out,
-      eval_expr e m a v ->
-      is_true v (typeof a) ->
-      exec_stmt e m s t m' out' ->
-      out_break_or_return out' out ->
-      exec_stmt e m (Swhile a s)
-                t m' out
-  | exec_Swhile_loop: forall e m a s v t1 m1 out1 t2 m2 out,
-      eval_expr e m a v ->
-      is_true v (typeof a) ->
-      exec_stmt e m s t1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      exec_stmt e m1 (Swhile a s) t2 m2 out ->
-      exec_stmt e m (Swhile a s)
-                (t1 ** t2) m2 out
-  | exec_Sdowhile_false: forall e m s a t m1 out1 v,
-      exec_stmt e m s t m1 out1 ->
-      out_normal_or_continue out1 ->
-      eval_expr e m1 a v ->
-      is_false v (typeof a) ->
-      exec_stmt e m (Sdowhile a s)
-                t m1 Out_normal
-  | exec_Sdowhile_stop: forall e m s a t m1 out1 out,
-      exec_stmt e m s t m1 out1 ->
-      out_break_or_return out1 out ->
-      exec_stmt e m (Sdowhile a s)
-                t m1 out
-  | exec_Sdowhile_loop: forall e m s a m1 m2 t1 t2 out out1 v,
-      exec_stmt e m s t1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      eval_expr e m1 a v ->
-      is_true v (typeof a) ->
-      exec_stmt e m1 (Sdowhile a s) t2 m2 out ->
-      exec_stmt e m (Sdowhile a s) 
-                (t1 ** t2) m2 out
-  | exec_Sfor_start: forall e m s a1 a2 a3 out m1 m2 t1 t2,
-      a1 <> Sskip ->
-      exec_stmt e m a1 t1 m1 Out_normal ->
-      exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out ->
-      exec_stmt e m (Sfor a1 a2 a3 s) 
-                (t1 ** t2) m2 out
-  | exec_Sfor_false: forall e m s a2 a3 v,
-      eval_expr e m a2 v ->
-      is_false v (typeof a2) ->
-      exec_stmt e m (Sfor Sskip a2 a3 s)
-               E0 m Out_normal
-  | exec_Sfor_stop: forall e m s a2 a3 v m1 t out1 out,
-      eval_expr e m a2 v ->
-      is_true v (typeof a2) ->
-      exec_stmt e m s t m1 out1 ->
-      out_break_or_return out1 out ->
-      exec_stmt e m (Sfor Sskip a2 a3 s)
-                t m1 out
-  | exec_Sfor_loop: forall e m s a2 a3 v m1 m2 m3 t1 t2 t3 out1 out,
-      eval_expr e m a2 v ->
-      is_true v (typeof a2) ->
-      exec_stmt e m s t1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      exec_stmt e m1 a3 t2 m2 Out_normal ->
-      exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out ->
-      exec_stmt e m (Sfor Sskip a2 a3 s)
-                (t1 ** t2 ** t3) m3 out
-  | exec_Sswitch:   forall e m a t n sl m1 out,
-      eval_expr e m a (Vint n) ->
-      exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out ->
-      exec_stmt e m (Sswitch a sl)
-                t m1 (outcome_switch out)
-
-(** [eval_funcall m1 fd args t m2 res] describes the invocation of
-  function [fd] with arguments [args].  [res] is the value returned
-  by the call.  *)
-
-with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
-  | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4,
-      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      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_return) vres ->
-      Mem.free_list m3 (blocks_of_env e) = Some m4 ->
-      eval_funcall m (Internal f) vargs t m4 vres
-  | eval_funcall_external: forall m ef targs tres vargs t vres m',
-      external_call ef ge vargs m t vres m' ->
-      eval_funcall m (External ef targs tres) vargs t m' vres.
-
-Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
-  with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
-
-(** ** Big-step semantics for diverging statements and functions *)
-
-(** Coinductive semantics for divergence.
-  [execinf_stmt ge e m s t] holds if the execution of statement [s]
-  diverges, i.e. loops infinitely.  [t] is the possibly infinite
-  trace of observable events performed during the execution. *)
-
-CoInductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
-  | execinf_Scall_none:   forall e m a al vf vargs f t,
-      eval_expr e m a vf ->
-      eval_exprlist e m al vargs ->
-      Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
-      evalinf_funcall m f vargs t ->
-      execinf_stmt e m (Scall None a al) t
-  | execinf_Scall_some:   forall e m lhs a al loc ofs vf vargs f t,
-      eval_lvalue e m lhs loc ofs ->
-      eval_expr e m a vf ->
-      eval_exprlist e m al vargs ->
-      Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
-      evalinf_funcall m f vargs t ->
-      execinf_stmt e m (Scall (Some lhs) a al) t
-  | execinf_Sseq_1:   forall e m s1 s2 t,
-      execinf_stmt e m s1 t ->
-      execinf_stmt e m (Ssequence s1 s2) t
-  | execinf_Sseq_2:   forall e m s1 s2 t1 m1 t2,
-      exec_stmt e m s1 t1 m1 Out_normal ->
-      execinf_stmt e m1 s2 t2 ->
-      execinf_stmt e m (Ssequence s1 s2) (t1 *** t2)
-  | execinf_Sifthenelse_true: forall e m a s1 s2 v1 t,
-      eval_expr e m a v1 ->
-      is_true v1 (typeof a) ->
-      execinf_stmt e m s1 t ->
-      execinf_stmt e m (Sifthenelse a s1 s2) t
-  | execinf_Sifthenelse_false: forall e m a s1 s2 v1 t,
-      eval_expr e m a v1 ->
-      is_false v1 (typeof a) ->
-      execinf_stmt e m s2 t ->
-      execinf_stmt e m (Sifthenelse a s1 s2) t
-  | execinf_Swhile_body: forall e m a v s t,
-      eval_expr e m a v ->
-      is_true v (typeof a) ->
-      execinf_stmt e m s t ->
-      execinf_stmt e m (Swhile a s) t
-  | execinf_Swhile_loop: forall e m a s v t1 m1 out1 t2,
-      eval_expr e m a v ->
-      is_true v (typeof a) ->
-      exec_stmt e m s t1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      execinf_stmt e m1 (Swhile a s) t2 ->
-      execinf_stmt e m (Swhile a s) (t1 *** t2)
-  | execinf_Sdowhile_body: forall e m s a t,
-      execinf_stmt e m s t ->
-      execinf_stmt e m (Sdowhile a s) t
-  | execinf_Sdowhile_loop: forall e m s a m1 t1 t2 out1 v,
-      exec_stmt e m s t1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      eval_expr e m1 a v ->
-      is_true v (typeof a) ->
-      execinf_stmt e m1 (Sdowhile a s) t2 ->
-      execinf_stmt e m (Sdowhile a s) (t1 *** t2)
-  | execinf_Sfor_start_1: forall e m s a1 a2 a3 t,
-      execinf_stmt e m a1 t ->
-      execinf_stmt e m (Sfor a1 a2 a3 s) t
-  | execinf_Sfor_start_2: forall e m s a1 a2 a3 m1 t1 t2,
-      a1 <> Sskip ->
-      exec_stmt e m a1 t1 m1 Out_normal ->
-      execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 ->
-      execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2)
-  | execinf_Sfor_body: forall e m s a2 a3 v t,
-      eval_expr e m a2 v ->
-      is_true v (typeof a2) ->
-      execinf_stmt e m s t ->
-      execinf_stmt e m (Sfor Sskip a2 a3 s) t
-  | execinf_Sfor_next: forall e m s a2 a3 v m1 t1 t2 out1,
-      eval_expr e m a2 v ->
-      is_true v (typeof a2) ->
-      exec_stmt e m s t1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      execinf_stmt e m1 a3 t2 ->
-      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2)
-  | execinf_Sfor_loop: forall e m s a2 a3 v m1 m2 t1 t2 t3 out1,
-      eval_expr e m a2 v ->
-      is_true v (typeof a2) ->
-      exec_stmt e m s t1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      exec_stmt e m1 a3 t2 m2 Out_normal ->
-      execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 ->
-      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3)
-  | execinf_Sswitch:   forall e m a t n sl,
-      eval_expr e m a (Vint n) ->
-      execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t ->
-      execinf_stmt e m (Sswitch a sl) t
-
-(** [evalinf_funcall ge m fd args t] holds if the invocation of function
-    [fd] on arguments [args] diverges, with observable trace [t]. *)
-
-with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
-  | evalinf_funcall_internal: forall m f vargs t e m1 m2,
-      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      bind_parameters e m1 f.(fn_params) vargs m2 ->
-      execinf_stmt e m2 f.(fn_body) t ->
-      evalinf_funcall m (Internal f) vargs t.
+Definition step (S: state) (t: trace) (S': state) : Prop :=
+  estep S t S' \/ sstep S t S'.
 
 End SEMANTICS.
 
@@ -1232,6 +1169,7 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
+      type_of_fundef f = Tfunction Tnil (Tint I32 Signed) ->
       initial_state p (Callstate f nil Kstop m0).
 
 (** A final state is a [Returnstate] with an empty continuation. *)
@@ -1248,500 +1186,3 @@ Inductive final_state: state -> int -> Prop :=
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
 
-(** Big-step execution of a whole program.  *)
-
-Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
-  | bigstep_program_terminates_intro: forall b f m0 m1 t r,
-      let ge := Genv.globalenv p in 
-      Genv.init_mem p = Some m0 ->
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      eval_funcall ge m0 f nil t m1 (Vint r) ->
-      bigstep_program_terminates p t r.
-
-Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
-  | bigstep_program_diverges_intro: forall b f m0 t,
-      let ge := Genv.globalenv p in 
-      Genv.init_mem p = Some m0 ->
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      evalinf_funcall ge m0 f nil t ->
-      bigstep_program_diverges p t.
-
-(** * Implication from big-step semantics to transition semantics *)
-
-Section BIGSTEP_TO_TRANSITIONS.
-
-Variable prog: program.
-Let ge : genv := Genv.globalenv prog.
-
-Definition exec_stmt_eval_funcall_ind
-  (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop)
-  (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) :=
-  fun a b c d e f g h i j k l m n o p q r s t u v w x y =>
-  conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y)
-       (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y).
-
-Inductive outcome_state_match
-       (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
-  | osm_normal:
-      outcome_state_match e m f k Out_normal (State f Sskip k e m)
-  | osm_break:
-      outcome_state_match e m f k Out_break (State f Sbreak k e m)
-  | osm_continue:
-      outcome_state_match e m f k Out_continue (State f Scontinue k e m)
-  | osm_return_none: forall k',
-      call_cont k' = call_cont k ->
-      outcome_state_match e m f k 
-        (Out_return None) (State f (Sreturn None) k' e m)
-  | osm_return_some: forall a v k',
-      call_cont k' = call_cont k ->
-      eval_expr ge e m a v ->
-      outcome_state_match e m f k
-        (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m).
-
-Lemma is_call_cont_call_cont:
-  forall k, is_call_cont k -> call_cont k = k.
-Proof.
-  destruct k; simpl; intros; contradiction || auto.
-Qed.
-
-Lemma exec_stmt_eval_funcall_steps:
-  (forall e m s t m' out,
-   exec_stmt ge e m s t m' out ->
-   forall f k, exists S,
-   star step ge (State f s k e m) t S
-   /\ outcome_state_match e m' f k out S)
-/\
-  (forall m fd args t m' res,
-   eval_funcall ge m fd args t m' res ->
-   forall k,
-   is_call_cont k ->
-   star step ge (Callstate fd args k m) t (Returnstate res k m')).
-Proof.
-  apply exec_stmt_eval_funcall_ind; intros.
-
-(* skip *)
-  econstructor; split. apply star_refl. constructor.
-
-(* assign *)
-  econstructor; split. apply star_one. econstructor; eauto. constructor.
-
-(* call none *)
-  econstructor; split.
-  eapply star_left. econstructor; eauto. 
-  eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq.
-  constructor.
-
-(* call some *)
-  econstructor; split.
-  eapply star_left. econstructor; eauto. 
-  eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq.
-  constructor.
-
-(* sequence 2 *)
-  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1.
-  destruct (H2 f k) as [S2 [A2 B2]]. 
-  econstructor; split.
-  eapply star_left. econstructor.
-  eapply star_trans. eexact A1. 
-  eapply star_left. constructor. eexact A2.
-  reflexivity. reflexivity. traceEq.
-  auto.
-
-(* sequence 1 *)
-  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
-  set (S2 :=
-    match out with
-    | Out_break => State f Sbreak k e m1
-    | Out_continue => State f Scontinue k e m1
-    | _ => S1
-    end).
-  exists S2; split.
-  eapply star_left. econstructor.
-  eapply star_trans. eexact A1.
-  unfold S2; inv B1.
-    congruence.
-    apply star_one. apply step_break_seq.
-    apply star_one. apply step_continue_seq.
-    apply star_refl.
-    apply star_refl.
-  reflexivity. traceEq.
-  unfold S2; inv B1; congruence || econstructor; eauto.
-
-(* ifthenelse true *)
-  destruct (H2 f k) as [S1 [A1 B1]].
-  exists S1; split.
-  eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq.
-  auto.
-
-(* ifthenelse false *)
-  destruct (H2 f k) as [S1 [A1 B1]].
-  exists S1; split.
-  eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq.
-  auto.
-
-(* return none *)
-  econstructor; split. apply star_refl. constructor. auto.
-
-(* return some *)
-  econstructor; split. apply star_refl. econstructor; eauto.
-
-(* break *)
-  econstructor; split. apply star_refl. constructor.
-
-(* continue *)
-  econstructor; split. apply star_refl. constructor.
-
-(* while false *)
-  econstructor; split.
-  apply star_one. eapply step_while_false; eauto. 
-  constructor.
-
-(* while stop *)
-  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
-  set (S2 :=
-    match out' with
-    | Out_break => State f Sskip k e m'
-    | _ => S1
-    end).
-  exists S2; split.
-  eapply star_left. eapply step_while_true; eauto. 
-  eapply star_trans. eexact A1.
-  unfold S2. inversion H3; subst.
-  inv B1. apply star_one. constructor.    
-  apply star_refl.
-  reflexivity. traceEq.
-  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
-
-(* while loop *)
-  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
-  destruct (H5 f k) as [S2 [A2 B2]].
-  exists S2; split.
-  eapply star_left. eapply step_while_true; eauto.
-  eapply star_trans. eexact A1.
-  eapply star_left.
-  inv H3; inv B1; apply step_skip_or_continue_while; auto.
-  eexact A2.
-  reflexivity. reflexivity. traceEq.
-  auto.
-
-(* dowhile false *)
-  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
-  exists (State f Sskip k e m1); split.
-  eapply star_left. constructor. 
-  eapply star_right. eexact A1.
-  inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto.
-  reflexivity. traceEq. 
-  constructor.
-
-(* dowhile stop *)
-  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
-  set (S2 :=
-    match out1 with
-    | Out_break => State f Sskip k e m1
-    | _ => S1
-    end).
-  exists S2; split.
-  eapply star_left. apply step_dowhile. 
-  eapply star_trans. eexact A1.
-  unfold S2. inversion H1; subst.
-  inv B1. apply star_one. constructor.
-  apply star_refl.
-  reflexivity. traceEq.
-  unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto.
-
-(* dowhile loop *)
-  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
-  destruct (H5 f k) as [S2 [A2 B2]].
-  exists S2; split.
-  eapply star_left. apply step_dowhile. 
-  eapply star_trans. eexact A1.
-  eapply star_left.
-  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
-  eexact A2.
-  reflexivity. reflexivity. traceEq.
-  auto.
-
-(* for start *)
-  destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1.
-  destruct (H3 f k) as [S2 [A2 B2]].
-  exists S2; split.
-  eapply star_left. apply step_for_start; auto.   
-  eapply star_trans. eexact A1.
-  eapply star_left. constructor. eexact A2.
-  reflexivity. reflexivity. traceEq.
-  auto.
-
-(* for false *)
-  econstructor; split.
-  eapply star_one. eapply step_for_false; eauto. 
-  constructor.
-
-(* for stop *)
-  destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
-  set (S2 :=
-    match out1 with
-    | Out_break => State f Sskip k e m1
-    | _ => S1
-    end).
-  exists S2; split.
-  eapply star_left. eapply step_for_true; eauto. 
-  eapply star_trans. eexact A1.
-  unfold S2. inversion H3; subst.
-  inv B1. apply star_one. constructor. 
-  apply star_refl.
-  reflexivity. traceEq.
-  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
-
-(* for loop *)
-  destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
-  destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2.
-  destruct (H7 f k) as [S3 [A3 B3]].
-  exists S3; split.
-  eapply star_left. eapply step_for_true; eauto. 
-  eapply star_trans. eexact A1.
-  eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1).
-  inv H3; inv B1.
-  apply star_one. constructor. auto. 
-  apply star_one. constructor. auto. 
-  eapply star_trans. eexact A2. 
-  eapply star_left. constructor.
-  eexact A3.
-  reflexivity. reflexivity. reflexivity. reflexivity. traceEq.
-  auto.
-
-(* switch *)
-  destruct (H1 f (Kswitch k)) as [S1 [A1 B1]].
-  set (S2 :=
-    match out with
-    | Out_normal => State f Sskip k e m1
-    | Out_break => State f Sskip k e m1
-    | Out_continue => State f Scontinue k e m1
-    | _ => S1
-    end).
-  exists S2; split.
-  eapply star_left. eapply step_switch; eauto. 
-  eapply star_trans. eexact A1. 
-  unfold S2; inv B1.
-    apply star_one. constructor. auto. 
-    apply star_one. constructor. auto. 
-    apply star_one. constructor. 
-    apply star_refl.
-    apply star_refl.
-  reflexivity. traceEq.
-  unfold S2. inv B1; simpl; econstructor; eauto.
-
-(* call internal *)
-  destruct (H2 f k) as [S1 [A1 B1]].
-  eapply star_left. eapply step_internal_function; eauto.
-  eapply star_right. eexact A1. 
-  inv B1; simpl in H3; try contradiction.
-  (* Out_normal *)
-  assert (fn_return f = Tvoid /\ vres = Vundef).
-    destruct (fn_return f); auto || contradiction.
-  destruct H6. subst vres. apply step_skip_call; auto.
-  (* Out_return None *)
-  assert (fn_return f = Tvoid /\ vres = Vundef).
-    destruct (fn_return f); auto || contradiction.
-  destruct H7. subst vres.
-  rewrite <- (is_call_cont_call_cont k H5). rewrite <- H6.
-  apply step_return_0; auto.
-  (* Out_return Some *)
-  destruct H3. subst vres.
-  rewrite <- (is_call_cont_call_cont k H5). rewrite <- H6.
-  eapply step_return_1; eauto.
-  reflexivity. traceEq.
-
-(* call external *)
-  apply star_one. apply step_external_function; auto. 
-Qed.
-
-Lemma exec_stmt_steps:
-   forall e m s t m' out,
-   exec_stmt ge e m s t m' out ->
-   forall f k, exists S,
-   star step ge (State f s k e m) t S
-   /\ outcome_state_match e m' f k out S.
-Proof (proj1 exec_stmt_eval_funcall_steps).
-
-Lemma eval_funcall_steps:
-   forall m fd args t m' res,
-   eval_funcall ge m fd args t m' res ->
-   forall k,
-   is_call_cont k ->
-   star step ge (Callstate fd args k m) t (Returnstate res k m').
-Proof (proj2 exec_stmt_eval_funcall_steps).
-
-Definition order (x y: unit) := False.
-
-Lemma evalinf_funcall_forever:
-  forall m fd args T k,
-  evalinf_funcall ge m fd args T ->
-  forever_N step order ge tt (Callstate fd args k m) T.
-Proof.
-  cofix CIH_FUN.
-  assert (forall e m s T f k,
-          execinf_stmt ge e m s T ->
-          forever_N step order ge tt (State f s k e m) T).
-  cofix CIH_STMT.
-  intros. inv H.
-
-(* call none *)
-  eapply forever_N_plus.
-  apply plus_one. eapply step_call_none; eauto. 
-  apply CIH_FUN. eauto. traceEq.
-(* call some *)
-  eapply forever_N_plus.
-  apply plus_one. eapply step_call_some; eauto. 
-  apply CIH_FUN. eauto. traceEq.
-
-(* seq 1 *)
-  eapply forever_N_plus.
-  apply plus_one. econstructor.
-  apply CIH_STMT; eauto. traceEq.
-(* seq 2 *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]].
-  inv B1.
-  eapply forever_N_plus.
-  eapply plus_left. constructor. eapply star_trans. eexact A1. 
-  apply star_one. constructor. reflexivity. reflexivity.
-  apply CIH_STMT; eauto. traceEq.
-
-(* ifthenelse true *)
-  eapply forever_N_plus.
-  apply plus_one. eapply step_ifthenelse_true; eauto. 
-  apply CIH_STMT; eauto. traceEq.
-(* ifthenelse false *)
-  eapply forever_N_plus.
-  apply plus_one. eapply step_ifthenelse_false; eauto. 
-  apply CIH_STMT; eauto. traceEq.
-
-(* while body *)
-  eapply forever_N_plus.
-  eapply plus_one. eapply step_while_true; eauto.
-  apply CIH_STMT; eauto. traceEq.
-(* while loop *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]].
-  eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1).
-  eapply plus_left. eapply step_while_true; eauto.
-  eapply star_right. eexact A1.
-  inv H3; inv B1; apply step_skip_or_continue_while; auto. 
-  reflexivity. reflexivity.
-  apply CIH_STMT; eauto. traceEq.
-
-(* dowhile body *)
-  eapply forever_N_plus.
-  eapply plus_one. eapply step_dowhile.
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* dowhile loop *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]].
-  eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1).
-  eapply plus_left. eapply step_dowhile. 
-  eapply star_right. eexact A1.
-  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. 
-  reflexivity. reflexivity.
-  apply CIH_STMT. eauto. 
-  traceEq.
-
-(* for start 1 *)
-  assert (a1 <> Sskip). red; intros; subst. inv H0.
-  eapply forever_N_plus.
-  eapply plus_one. apply step_for_start; auto. 
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* for start 2 *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]].
-  inv B1.
-  eapply forever_N_plus.
-  eapply plus_left. eapply step_for_start; eauto. 
-  eapply star_right. eexact A1.
-  apply step_skip_seq. 
-  reflexivity. reflexivity.
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* for body *)
-  eapply forever_N_plus.
-  apply plus_one. eapply step_for_true; eauto. 
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* for next *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
-  eapply forever_N_plus.
-  eapply plus_left. eapply step_for_true; eauto.
-  eapply star_trans. eexact A1.
-  apply star_one.
-  inv H3; inv B1; apply step_skip_or_continue_for2; auto.
-  reflexivity. reflexivity. 
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* for body *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
-  destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]].
-  inv B2.
-  eapply forever_N_plus.
-  eapply plus_left. eapply step_for_true; eauto. 
-  eapply star_trans. eexact A1.
-  eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto.
-  eapply star_right. eexact A2. 
-  constructor. 
-  reflexivity. reflexivity. reflexivity. reflexivity.  
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* switch *)
-  eapply forever_N_plus.
-  eapply plus_one. eapply step_switch; eauto.
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* call internal *)
-  intros. inv H0.
-  eapply forever_N_plus.
-  eapply plus_one. econstructor; eauto. 
-  apply H; eauto.
-  traceEq.
-Qed.
-
-Theorem bigstep_program_terminates_exec:
-  forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
-Proof.
-  intros. inv H. 
-  econstructor.
-  econstructor. eauto. eauto. eauto.
-  apply eval_funcall_steps. eauto. red; auto. 
-  econstructor.
-Qed.
-
-Theorem bigstep_program_diverges_exec:
-  forall T, bigstep_program_diverges prog T ->
-  exec_program prog (Reacts T) \/
-  exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
-Proof.
-  intros. inv H.
-  set (st := Callstate f nil Kstop m0).
-  assert (forever step ge0 st T). 
-    eapply forever_N_forever with (order := order).
-    red; intros. constructor; intros. red in H. elim H.
-    eapply evalinf_funcall_forever; eauto. 
-  destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
-  as [A | [t [s' [T' [B [C D]]]]]]. 
-  left. econstructor. econstructor; eauto. eauto.
-  right. exists t. split.
-  econstructor. econstructor; eauto. eauto. auto. 
-  subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
-Qed.
-
-End BIGSTEP_TO_TRANSITIONS.
-
-
-
-
-
-