diff options
Diffstat (limited to '')
| -rw-r--r-- | miasm2/ir/translators/z3_ir.py | 6 | ||||
| -rw-r--r-- | test/ir/translators/z3_ir.py | 8 |
2 files changed, 12 insertions, 2 deletions
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index db038fe1..6f0b1aef 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -3,6 +3,7 @@ import operator import z3 +from miasm2.core.asmbloc import asm_label from miasm2.ir.translators.translator import Translator log = logging.getLogger("translator_z3") @@ -117,7 +118,10 @@ class TranslatorZ3(Translator): @classmethod def from_ExprId(cls, expr): - return z3.BitVec(str(expr), expr.size) + if isinstance(expr.name, asm_label) and expr.name.offset is not None: + return z3.BitVecVal(expr.name.offset, expr.size) + else: + return z3.BitVec(str(expr), expr.size) @classmethod def from_ExprMem(cls, expr): 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." |