diff options
| author | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 20:14:10 +0100 |
|---|---|---|
| committer | Tim Blazytko <tim.blazytko@rub.de> | 2016-02-01 20:14:10 +0100 |
| commit | 8305597a30ff2f91f97e4ac259607899049a33da (patch) | |
| tree | 51d51c85db66fa57c6cd73264bdf7fea7a0e29a2 | |
| parent | dddd55b2b707cd0a908aa035523980ce88997d2a (diff) | |
| download | miasm-8305597a30ff2f91f97e4ac259607899049a33da.tar.gz miasm-8305597a30ff2f91f97e4ac259607899049a33da.zip | |
z3 translator: fixed regression tests
| -rw-r--r-- | test/ir/translators/z3_ir.py | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index cf29635e..e080c7f5 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -151,18 +151,21 @@ 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))) +bsf1 = Translator.to_language('z3').from_expr(ExprOp("bsf", ExprInt(0x1138, 32))) +bsf2 = z3.BitVecVal(3, 32) +assert(equiv(bsf1, bsf2)) # bsr(0x11300) == 0x10 -assert(equiv(ExprOp("bsr", ExprInt(0x11300)), ExprInt(0x10, 32))) +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) -assert(equiv(ExprOp("bsf", ExprInt(0x80000)), ExprInt(0x13, 32))) - +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." |