diff options
| author | Ajax <commial@gmail.com> | 2017-04-21 17:31:29 +0200 |
|---|---|---|
| committer | Ajax <commial@gmail.com> | 2017-04-21 17:31:29 +0200 |
| commit | b7bf1132834cec1d7d90fa0e01dfea66d1eb0722 (patch) | |
| tree | d981aee981972396ed3219952e964c4d422b6314 | |
| parent | 7a9ba958c66c80b843bdd571f6989a8bb3e98dce (diff) | |
| download | miasm-b7bf1132834cec1d7d90fa0e01dfea66d1eb0722.tar.gz miasm-b7bf1132834cec1d7d90fa0e01dfea66d1eb0722.zip | |
DSE: support absence of z3
| -rw-r--r-- | miasm2/analysis/dse.py | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/miasm2/analysis/dse.py b/miasm2/analysis/dse.py index 290015ea..7fdc5035 100644 --- a/miasm2/analysis/dse.py +++ b/miasm2/analysis/dse.py @@ -49,7 +49,10 @@ Here are a few remainings TODO: from collections import namedtuple -import z3 +try: + import z3 +except ImportError: + z3 = None from miasm2.expression.expression import ExprMem, ExprInt, ExprCompose, \ ExprAff, ExprId @@ -447,7 +450,11 @@ class DSEPathConstraint(DSEEngine): @machine: Machine of the targeted architecture instance @produce_solution: (optional) if set, new solutions will be computed""" super(DSEPathConstraint, self).__init__(machine, **kwargs) - self.path_constraint = set() + + # Dependency check + assert z3 is not None + + # Init PathConstraint specifics structures self.produce_solution = produce_solution self.cur_solver = z3.Solver() self.new_solutions = {} # destination -> set of model |