From eb7c8587f462adca878088ef5f610c81734efc70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 19 Sep 2006 15:13:42 +0000 Subject: Meilleure compilation de la negation booleenne git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csharpminor.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'cfrontend/Csharpminor.v') diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 016fab4d..f1d22d7e 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -37,6 +37,7 @@ Inductive operation : Set := | Ocast8signed: operation (**r 8-bit sign extension *) | Ocast16unsigned: operation (**r 16-bit zero extension *) | Ocast16signed: operation (**r 16-bit sign extension *) + | Onotbool: operation (**r boolean negation *) | Onotint: operation (**r bitwise complement *) | Oadd: operation (**r integer addition *) | Osub: operation (**r integer subtraction *) @@ -214,6 +215,8 @@ Definition eval_operation (op: operation) (vl: list val) (m: mem): option val := | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1)) | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1)) | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1)) + | Onotbool, Vint n1 :: nil => Some (Val.of_bool (Int.eq n1 Int.zero)) + | Onotbool, Vptr b1 n1 :: nil => Some (Vfalse) | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1)) | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) -- cgit