about summary refs log tree commit diff stats
path: root/test/ir/translators/z3_ir.py
diff options
context:
space:
mode:
authorFlorent Monjalet <florent.monjalet@gmail.com>2015-03-24 00:36:58 +0100
committerFlorent Monjalet <florent.monjalet@gmail.com>2015-03-24 00:36:58 +0100
commita326cba3e548313a947594370bc97b879a27c63b (patch)
tree2fab20e0977b54863792c08b665da992144df859 /test/ir/translators/z3_ir.py
parentc8590c5985292d02e2989fac530ea2d3a30535f1 (diff)
downloadmiasm-a326cba3e548313a947594370bc97b879a27c63b.tar.gz
miasm-a326cba3e548313a947594370bc97b879a27c63b.zip
TranslatorZ3: Better handling of asm_labels (translating to BitVecVal when possible)
Diffstat (limited to '')
-rw-r--r--test/ir/translators/z3_ir.py8
1 files changed, 7 insertions, 1 deletions
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index fa656ed0..6e483d61 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -139,9 +139,15 @@ for miasm_int, res in [(five, -5), (four, -4)]:
     assert equiv(ez3, z3_e6)
 
 # --------------------------------------------------------------------------
-# Should just not throw anything
 e7 = ExprId(asm_label("label_histoire", 0xdeadbeef), 32)
 ez3 = Translator.to_language('z3').from_expr(e7)
+z3_e7 = z3.BitVecVal(0xdeadbeef, 32)
+assert equiv(ez3, z3_e7)
+
+# Should just not throw anything to pass
+e8 = ExprId(asm_label("label_jambe"), 32)
+ez3 = Translator.to_language('z3').from_expr(e8)
+assert not equiv(ez3, z3_e7)
 
 print "TranslatorZ3 tests are OK."