diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-28 14:56:39 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-28 14:56:39 +0000 |
| commit | 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 (patch) | |
| tree | c70dda532a974a7b62969c6b199b80d65784dc91 /cfrontend/Csem.v | |
| parent | b54721f58c2ecb65ce554d8b34f214d5121a2b0c (diff) | |
| download | compcert-kvx-14a9bb4b267eeead8cd9503ee19e860a8bc0d763.tar.gz compcert-kvx-14a9bb4b267eeead8cd9503ee19e860a8bc0d763.zip | |
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
Diffstat (limited to 'cfrontend/Csem.v')
| -rw-r--r-- | cfrontend/Csem.v | 7 |
1 files changed, 4 insertions, 3 deletions
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))) |