diff options
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)) |