diff options
Diffstat (limited to 'cfrontend/Csem.v')
-rw-r--r-- | cfrontend/Csem.v | 39 |
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 |