diff options
Diffstat (limited to 'test/ir/translators/z3_ir.py')
| -rw-r--r-- | test/ir/translators/z3_ir.py | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index a4fa7410..e080c7f5 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -149,5 +149,23 @@ e8 = ExprId(asm_label("label_jambe"), 32) ez3 = Translator.to_language('z3').from_expr(e8) assert not equiv(ez3, z3_e7) +# -------------------------------------------------------------------------- +# bsr, bsf + +# bsf(0x1138) == 3 +bsf1 = Translator.to_language('z3').from_expr(ExprOp("bsf", ExprInt(0x1138, 32))) +bsf2 = z3.BitVecVal(3, 32) +assert(equiv(bsf1, bsf2)) + +# bsr(0x11300) == 0x10 +bsr1 = Translator.to_language('z3').from_expr(ExprOp("bsr", ExprInt(0x11300, 32))) +bsr2 = z3.BitVecVal(0x10, 32) +assert(equiv(bsr1, bsr2)) + +# bsf(0x80000) == bsr(0x80000) +bsf3 = Translator.to_language('z3').from_expr(ExprOp("bsf", ExprInt(0x80000, 32))) +bsr3 = Translator.to_language('z3').from_expr(ExprOp("bsr", ExprInt(0x80000, 32))) +assert(equiv(bsf3, bsr3)) + print "TranslatorZ3 tests are OK." |