diff options
| author | serpilliere <serpilliere@users.noreply.github.com> | 2016-02-02 20:09:21 +0100 |
|---|---|---|
| committer | serpilliere <serpilliere@users.noreply.github.com> | 2016-02-02 20:09:21 +0100 |
| commit | 147a217b64b3610cdd822b0f23ad2af8106960fd (patch) | |
| tree | a46cc5e1cfb19e4a8261eb2522db41184018b05d /test | |
| parent | 4fa1cd0a0f78f8a6b46a407a084d30c04aff6bd2 (diff) | |
| parent | ed0915266cb57950eb4457ad7269a8ab2c666d3c (diff) | |
| download | miasm-147a217b64b3610cdd822b0f23ad2af8106960fd.tar.gz miasm-147a217b64b3610cdd822b0f23ad2af8106960fd.zip | |
Merge pull request #318 from mrphrazer/translator_bsf_bsr
z3/smt2 translation for bsf and bsr
Diffstat (limited to 'test')
| -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." |