diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-19 15:13:42 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-19 15:13:42 +0000 |
| commit | eb7c8587f462adca878088ef5f610c81734efc70 (patch) | |
| tree | 6771c5be9d0d6048357be99c663ec64981ad63dd /cfrontend/Csharpminor.v | |
| parent | 165407527b1be7df6a376791719321c788e55149 (diff) | |
| download | compcert-kvx-eb7c8587f462adca878088ef5f610c81734efc70.tar.gz compcert-kvx-eb7c8587f462adca878088ef5f610c81734efc70.zip | |
Meilleure compilation de la negation booleenne
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Csharpminor.v')
| -rw-r--r-- | cfrontend/Csharpminor.v | 3 |
1 files changed, 3 insertions, 0 deletions
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)) |