diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:27:15 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:27:15 +0000 |
| commit | f4b41226d60ca57c5981b0a46e0a495152b5301f (patch) | |
| tree | fb3ea7a1cabfc5e4c56ecc1b60eeacd2883a8293 /backend/Op.v | |
| parent | f77e0ade09d8fd17add98c3bc4317627078f3aa8 (diff) | |
| download | compcert-f4b41226d60ca57c5981b0a46e0a495152b5301f.tar.gz compcert-f4b41226d60ca57c5981b0a46e0a495152b5301f.zip | |
Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore utilisee dans le front-end C.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Op.v')
| -rw-r--r-- | backend/Op.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/backend/Op.v b/backend/Op.v index 51b5e530..2094d597 100644 --- a/backend/Op.v +++ b/backend/Op.v @@ -94,7 +94,8 @@ Inductive operation : Set := | Omulsubf: operation (**r [rd = r1 * r2 - r3] *) | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) (*c Conversions between int and float: *) - | Ointoffloat: operation (**r [rd = int_of_float(r1)] *) + | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) + | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] *) | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *) | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] *) (*c Boolean tests: *) @@ -229,6 +230,8 @@ Definition eval_operation Some (Val.singleoffloat v1) | Ointoffloat, Vfloat f1 :: nil => Some (Vint (Float.intoffloat f1)) + | Ointuoffloat, Vfloat f1 :: nil => + Some (Vint (Float.intuoffloat f1)) | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1)) | Ofloatofintu, Vint n1 :: nil => @@ -506,6 +509,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omulsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat) | Osingleoffloat => (Tfloat :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) + | Ointuoffloat => (Tfloat :: nil, Tint) | Ofloatofint => (Tint :: nil, Tfloat) | Ofloatofintu => (Tint :: nil, Tfloat) | Ocmp c => (type_of_condition c, Tint) @@ -666,6 +670,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val : | Omulsubf, v1::v2::v3::nil => Val.subf (Val.mulf v1 v2) v3 | Osingleoffloat, v1::nil => Val.singleoffloat v1 | Ointoffloat, v1::nil => Val.intoffloat v1 + | Ointuoffloat, v1::nil => Val.intuoffloat v1 | Ofloatofint, v1::nil => Val.floatofint v1 | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ocmp c, _ => eval_condition_total c vl |