From f4b41226d60ca57c5981b0a46e0a495152b5301f Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 30 May 2008 12:27:15 +0000 Subject: 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 --- backend/Cminor.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'backend/Cminor.v') diff --git a/backend/Cminor.v b/backend/Cminor.v index df541a1..c1e3bd1 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -50,7 +50,8 @@ Inductive unary_operation : Set := | Onegf: unary_operation (**r float opposite *) | Oabsf: unary_operation (**r float absolute value *) | Osingleoffloat: unary_operation (**r float truncation *) - | Ointoffloat: unary_operation (**r integer to float *) + | Ointoffloat: unary_operation (**r signed integer to float *) + | Ointuoffloat: unary_operation (**r unsigned integer to float *) | Ofloatofint: unary_operation (**r float to signed integer *) | Ofloatofintu: unary_operation. (**r float to unsigned integer *) @@ -239,6 +240,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := | Oabsf, Vfloat f1 => Some (Vfloat (Float.abs f1)) | Osingleoffloat, _ => Some (Val.singleoffloat arg) | Ointoffloat, Vfloat f1 => Some (Vint (Float.intoffloat f1)) + | Ointuoffloat, Vfloat f1 => Some (Vint (Float.intuoffloat f1)) | Ofloatofint, Vint n1 => Some (Vfloat (Float.floatofint n1)) | Ofloatofintu, Vint n1 => Some (Vfloat (Float.floatofintu n1)) | _, _ => None -- cgit v1.2.3