From 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Oct 2010 14:56:39 +0000 Subject: Float.intoffloat and Float.intuoffloat are now partial functions. (May fail if float is too big to be converted.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csem.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'cfrontend/Csem.v') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 742a969a..927cd69d 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -49,7 +49,7 @@ Definition cast_int_float (si : signedness) (i: int) : float := | Unsigned => Float.floatofintu i end. -Definition cast_float_int (si : signedness) (f: float) : int := +Definition cast_float_int (si : signedness) (f: float) : option int := match si with | Signed => Float.intoffloat f | Unsigned => Float.intuoffloat f @@ -75,9 +75,10 @@ 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_fi: forall f sz1 sz2 si2 i, (**r float to int *) + cast_float_int si2 f = Some i -> cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2) - (Vint (cast_int_int sz2 si2 (cast_float_int si2 f))) + (Vint (cast_int_int sz2 si2 i)) | 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))) -- cgit