diff options
| author | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 19:49:03 +0100 |
|---|---|---|
| committer | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 19:49:03 +0100 |
| commit | dddd55b2b707cd0a908aa035523980ce88997d2a (patch) | |
| tree | e05e46214e44bfbd881a095eaa658fc27b7185d0 | |
| parent | 6b0665ec2f0386fbd28e169cf098bc99242c6241 (diff) | |
| download | miasm-dddd55b2b707cd0a908aa035523980ce88997d2a.tar.gz miasm-dddd55b2b707cd0a908aa035523980ce88997d2a.zip | |
z3 translator: added regression tests for bsr and bsf
| -rw-r--r-- | test/ir/translators/z3_ir.py | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index a4fa7410..cf29635e 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -149,5 +149,20 @@ e8 = ExprId(asm_label("label_jambe"), 32) ez3 = Translator.to_language('z3').from_expr(e8) assert not equiv(ez3, z3_e7) +# -------------------------------------------------------------------------- +# bsr, bsf +e1 = ExprId("e1", 32) +e2 = ExprId("e2", 32) + +# bsf(0x1138) == 3 +assert(equiv(ExprOp("bsf", ExprInt(0x1138)), ExprInt(0x3, 32))) + +# bsr(0x11300) == 0x10 +assert(equiv(ExprOp("bsr", ExprInt(0x11300)), ExprInt(0x10, 32))) + +# bsf(0x80000) == bsr(0x80000) +assert(equiv(ExprOp("bsf", ExprInt(0x80000)), ExprInt(0x13, 32))) + + print "TranslatorZ3 tests are OK." |