From 07e07f549c9c40981538c0bf70d2de9ebe39f957 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 30 Apr 2018 16:44:50 +0200
Subject: [PATCH] Add method that checks if an interesting state is actually
 caused by a requires check

---
 mythril/analysis/modules/integer.py | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py
index f7d3c873..f0ec4a7c 100644
--- a/mythril/analysis/modules/integer.py
+++ b/mythril/analysis/modules/integer.py
@@ -284,3 +284,22 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth
         results += _search_children(statespace, child, expression, depth=depth + 1, max_depth=max_depth)
 
     return results
+
+
+def _check_requires(state, node, statespace, constraint):
+    """Checks if usage of overflowed statement results in a revert statement"""
+    instruction = state.get_current_instruction()
+    if instruction['opcode'] != 'JUMPI':
+        return False
+
+    children = \
+        [
+            statespace.nodes[edge.node_to]
+            for edge in statespace.edges
+            if edge.node_from == node.uid and _try_constraints(node.constraints, [constraint])
+        ]
+    for child in children:
+        opcodes = [s.get_current_instruction()['opcode'] for s in child.states]
+        if "REVERT" in opcodes:
+            return True
+    return False