|
|
@ -82,7 +82,7 @@ def _check_integer_overflow(statespace, state, node): |
|
|
|
logging.debug("[INTEGER_OVERFLOW] no model found") |
|
|
|
logging.debug("[INTEGER_OVERFLOW] no model found") |
|
|
|
return issues |
|
|
|
return issues |
|
|
|
|
|
|
|
|
|
|
|
if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1): |
|
|
|
if instruction['opcode'] != "MUL" and not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1) : |
|
|
|
return issues |
|
|
|
return issues |
|
|
|
|
|
|
|
|
|
|
|
# Build issue |
|
|
|
# Build issue |
|
|
@ -277,12 +277,13 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth |
|
|
|
continue |
|
|
|
continue |
|
|
|
results += element |
|
|
|
results += element |
|
|
|
|
|
|
|
|
|
|
|
# Recursively search children |
|
|
|
# Recursively search children |
|
|
|
children = \ |
|
|
|
children = \ |
|
|
|
[ |
|
|
|
[ |
|
|
|
statespace.nodes[edge.node_to] |
|
|
|
statespace.nodes[edge.node_to] |
|
|
|
for edge in statespace.edges |
|
|
|
for edge in statespace.edges |
|
|
|
if edge.node_from == node.uid and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None |
|
|
|
if edge.node_from == node.uid |
|
|
|
|
|
|
|
and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None |
|
|
|
] |
|
|
|
] |
|
|
|
|
|
|
|
|
|
|
|
for child in children: |
|
|
|
for child in children: |
|
|
|