Improved semantics of casts

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

1 files changed, 39 insertions, 0 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 5461353f..90bb2e31 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -61,6 +61,7 @@ Definition cast_float_float (sz: floatsize) (f: float) : float :=
   | F64 => f
   end.
 
+(*
 Definition neutral_for_cast (t: type) : bool :=
   match t with
   | Tint I32 sg => true
@@ -92,6 +93,44 @@ Function sem_cast (v: val) (t1 t2: type) : option val :=
   | _, _, _ =>
       None
   end.
+*)
+
+Function sem_cast (v: val) (t1 t2: type) : option val :=
+  match classify_cast t1 t2 with
+  | cast_case_neutral =>
+      match v with
+      | Vint _ | Vptr _ _ => Some v
+      | _ => None
+      end
+  | cast_case_i2i sz2 si2 =>
+      match v with
+      | Vint i => Some (Vint (cast_int_int sz2 si2 i))
+      | _ => None
+      end
+  | cast_case_f2f sz2 =>
+      match v with
+      | Vfloat f => Some (Vfloat (cast_float_float sz2 f))
+      | _ => None
+      end
+  | cast_case_i2f si1 sz2 =>
+      match v with
+      | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
+      | _ => None
+      end
+  | cast_case_f2i sz2 si2 =>
+      match v with
+      | Vfloat f =>
+          match cast_float_int si2 f with
+          | Some i => Some (Vint (cast_int_int sz2 si2 i))
+          | None => None
+          end
+      | _ => None
+      end
+  | cast_case_void =>
+      Some v
+  | cast_case_default =>
+      None
+  end.
 
 (** Interpretation of values as truth values.
   Non-zero integers, non-zero floats and non-null pointers are