about summary refs log tree commit diff stats
path: root/test
diff options
context:
space:
mode:
authorFlorent Monjalet <florent.monjalet@gmail.com>2015-03-23 23:16:29 +0100
committerFlorent Monjalet <florent.monjalet@gmail.com>2015-03-23 23:16:29 +0100
commita8ece9f5c56334c37caafb9eddcd38081d6b4464 (patch)
tree0e5329be0d00be85384679a6a9d19af2f28a87c4 /test
parentec67b96bbaf5810befc985fa3e46a68d1e864a77 (diff)
downloadmiasm-a8ece9f5c56334c37caafb9eddcd38081d6b4464.tar.gz
miasm-a8ece9f5c56334c37caafb9eddcd38081d6b4464.zip
TranslatorZ3: Handling 'parity' and '-' unary operators, and raising errors properly for other unhandled operators.
Diffstat (limited to '')
-rw-r--r--test/ir/translators/z3_ir.py16
1 files changed, 16 insertions, 0 deletions
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index 997a3da9..99d77c5a 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -119,5 +119,21 @@ ez3 = Translator.to_language('z3').from_expr(e5)
 z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five
 assert equiv(ez3, z3_e5)
 
+# --------------------------------------------------------------------------
+# Parity
+for miasm_int, res in [(five, 1), (four, 0)]:
+    e6 = ExprOp('parity', miasm_int)
+    ez3 = Translator.to_language('z3').from_expr(e6)
+    z3_e6 = z3.BitVecVal(res, 1)
+    assert equiv(ez3, z3_e6)
+
+# --------------------------------------------------------------------------
+# '-'
+for miasm_int, res in [(five, -5), (four, -4)]:
+    e6 = ExprOp('-', miasm_int)
+    ez3 = Translator.to_language('z3').from_expr(e6)
+    z3_e6 = z3.BitVecVal(res, 32)
+    assert equiv(ez3, z3_e6)
+
 print "TranslatorZ3 tests are OK."