Merge develop

mythril/analysis/modules/delegatecall.py

@@ -2,7 +2,7 @@
 import json
 import logging
 from copy import copy
-from typing import List, cast
+from typing import List, cast, Dict
 
 from mythril.analysis import solver
 from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT
@@ -27,7 +27,7 @@ class DelegateCallAnnotation(StateAnnotation):
             "retval_{}".format(call_state.get_current_instruction()["address"]), 256
         )
 
-    def get_issue(self, global_state: GlobalState, transaction_sequence: str) -> Issue:
+    def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue:
         """
         Returns Issue for the annotation
         :param global_state: Global State
@@ -58,7 +58,7 @@ class DelegateCallAnnotation(StateAnnotation):
             severity="Medium",
             description_head=description_head,
             description_tail=description_tail,
-            debug=transaction_sequence,
+            transaction_sequence=transaction_sequence,
             gas_used=(
                 global_state.mstate.min_gas_used,
                 global_state.mstate.max_gas_used,
@@ -128,8 +128,11 @@ def _analyze_states(state: GlobalState) -> List[Issue]:
                 transaction_sequence = solver.get_transaction_sequence(
                     state, state.mstate.constraints + [annotation.return_value == 1]
                 )
-                debug = json.dumps(transaction_sequence, indent=4)
-                issues.append(annotation.get_issue(state, transaction_sequence=debug))
+                issues.append(
+                    annotation.get_issue(
+                        state, transaction_sequence=transaction_sequence
+                    )
+                )
             except UnsatError:
                 continue
 

mythril/analysis/modules/ether_thief.py

@@ -95,8 +95,6 @@ class EtherThief(DetectionModule):
 
             transaction_sequence = solver.get_transaction_sequence(state, constraints)
 
-            debug = json.dumps(transaction_sequence, indent=4)
-
             issue = Issue(
                 contract=state.environment.active_account.contract_name,
                 function_name=state.environment.active_function_name,
@@ -109,7 +107,7 @@ class EtherThief(DetectionModule):
                 description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract"
                 + " account without previously having sent an equivalent amount of ETH to it. This is likely to be"
                 + " a vulnerability.",
-                debug=debug,
+                transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
         except UnsatError:

mythril/analysis/modules/exceptions.py

@@ -34,7 +34,6 @@ def _analyze_state(state) -> list:
         transaction_sequence = solver.get_transaction_sequence(
             state, state.mstate.constraints
         )
-        debug = json.dumps(transaction_sequence, indent=4)
 
         issue = Issue(
             contract=state.environment.active_account.contract_name,
@@ -46,7 +45,7 @@ def _analyze_state(state) -> list:
             description_head="A reachable exception has been detected.",
             description_tail=description_tail,
             bytecode=state.environment.code.bytecode,
-            debug=debug,
+            transaction_sequence=transaction_sequence,
             gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
         )
         return [issue]

mythril/analysis/modules/external_calls.py

@@ -47,7 +47,6 @@ def _analyze_state(state):
             constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF]
             transaction_sequence = solver.get_transaction_sequence(state, constraints)
 
-            debug = json.dumps(transaction_sequence, indent=4)
             description_head = "A call to a user-supplied address is executed."
             description_tail = (
                 "The callee address of an external message call can be set by "
@@ -66,7 +65,7 @@ def _analyze_state(state):
                 severity="Medium",
                 description_head=description_head,
                 description_tail=description_tail,
-                debug=debug,
+                transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
 
@@ -95,7 +94,7 @@ def _analyze_state(state):
                 severity="Low",
                 description_head=description_head,
                 description_tail=description_tail,
-                debug=debug,
+                transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
 

mythril/analysis/modules/integer.py

@@ -330,10 +330,9 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 description_head=self._get_description_head(annotation, _type),
                 description_tail=self._get_description_tail(annotation, _type),
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                transaction_sequence=transaction_sequence,
             )
 
-            issue.debug = json.dumps(transaction_sequence, indent=4)
-
             address = _get_address_from_state(ostate)
             self._overflow_cache[address] = True
             self._issues.append(issue)

mythril/analysis/modules/suicide.py

@@ -79,7 +79,6 @@ class SuicideModule(DetectionModule):
                 )
                 description_tail = "Arbitrary senders can kill this contract."
 
-            debug = json.dumps(transaction_sequence, indent=4)
             self._cache_address[instruction["address"]] = True
 
             issue = Issue(
@@ -92,7 +91,7 @@ class SuicideModule(DetectionModule):
                 severity="High",
                 description_head=description_head,
                 description_tail=description_tail,
-                debug=debug,
+                transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
             return [issue]

mythril/analysis/report.py

@@ -31,7 +31,7 @@ class Issue:
         severity=None,
         description_head="",
         description_tail="",
-        debug="",
+        transaction_sequence=None,
     ):
         """
 
@@ -55,7 +55,6 @@ class Issue:
         self.description_tail = description_tail
         self.description = "%s\n%s" % (description_head, description_tail)
         self.severity = severity
-        self.debug = debug
         self.swc_id = swc_id
         self.min_gas_used, self.max_gas_used = gas_used
         self.filename = None
@@ -64,6 +63,38 @@ class Issue:
         self.source_mapping = None
         self.discovery_time = time() - StartTime().global_start_time
         self.bytecode_hash = get_code_hash(bytecode)
+        self.transaction_sequence = transaction_sequence
+
+    @property
+    def transaction_sequence_users(self):
+        """ Returns the transaction sequence in json without pre-generated block data"""
+        return (
+            json.dumps(self.transaction_sequence, indent=4)
+            if self.transaction_sequence
+            else None
+        )
+
+    @property
+    def transaction_sequence_jsonv2(self):
+        """ Returns the transaction sequence in json with pre-generated block data"""
+        return (
+            json.dumps(self.add_block_data(self.transaction_sequence), indent=4)
+            if self.transaction_sequence
+            else None
+        )
+
+    @staticmethod
+    def add_block_data(transaction_sequence: Dict):
+        """ Adds sane block data to a transaction_sequence """
+        for step in transaction_sequence["steps"]:
+            step["gasLimit"] = "0x7d000"
+            step["gasPrice"] = "0x773594000"
+            step["blockCoinbase"] = "0xcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcb"
+            step["blockDifficulty"] = "0xa7d7343662e26"
+            step["blockGasLimit"] = "0x7d0000"
+            step["blockNumber"] = "0x66e393"
+            step["blockTime"] = "0x5bfa4639"
+        return transaction_sequence
 
     @property
     def as_dict(self):
@@ -79,7 +110,7 @@ class Issue:
             "function": self.function,
             "severity": self.severity,
             "address": self.address,
-            "debug": self.debug,
+            "tx_sequence": self.transaction_sequence_users,
             "min_gas_used": self.min_gas_used,
             "max_gas_used": self.max_gas_used,
             "sourceMap": self.source_mapping,
@@ -168,6 +199,7 @@ class Report:
         """
         name = self._file_name()
         template = Report.environment.get_template("report_as_text.jinja2")
+
         return template.render(
             filename=name, issues=self.sorted_issues(), verbose=self.verbose
         )
@@ -203,7 +235,9 @@ class Report:
                 title = SWC_TO_TITLE[issue.swc_id]
             except KeyError:
                 title = "Unspecified Security Issue"
-
+            extra = {"discoveryTime": int(issue.discovery_time * 10 ** 9)}
+            if issue.transaction_sequence_jsonv2:
+                extra["testCase"] = str(issue.transaction_sequence_jsonv2)
             _issues.append(
                 {
                     "swcID": "SWC-" + issue.swc_id,
@@ -214,7 +248,7 @@ class Report:
                     },
                     "severity": issue.severity,
                     "locations": [{"sourceMap": "%d:1:%d" % (issue.address, idx)}],
-                    "extra": {"discoveryTime": int(issue.discovery_time * 10 ** 9)},
+                    "extra": extra,
                 }
             )
         meta_data = self._get_exception_data()

mythril/analysis/solver.py

@@ -1,8 +1,13 @@
 """This module contains analysis module helpers to solve path constraints."""
+from typing import Dict, List, Union
 from z3 import sat, unknown, FuncInterp
 import z3
 
-from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import Account
+from mythril.laser.ethereum.state.constraints import Constraints
+from mythril.laser.ethereum.transaction import BaseTransaction
+from mythril.laser.smt import UGE, Optimize, symbol_factory
 from mythril.laser.ethereum.time_handler import time_handler
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
@@ -51,7 +56,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
 
 
 def pretty_print_model(model):
-    """
+    """ Pretty prints a z3 model
 
     :param model:
     :return:
@@ -74,7 +79,9 @@ def pretty_print_model(model):
     return ret
 
 
-def get_transaction_sequence(global_state, constraints):
+def get_transaction_sequence(
+    global_state: GlobalState, constraints: Constraints
+) -> Dict:
     """Generate concrete transaction sequence.
 
     :param global_state: GlobalState to generate transaction sequence for
@@ -83,55 +90,102 @@ def get_transaction_sequence(global_state, constraints):
 
     transaction_sequence = global_state.world_state.transaction_sequence
 
-    # gaslimit & gasprice don't exist yet
-    tx_template = {
-        "calldata": None,
-        "call_value": None,
-        "caller": "0xCA11EDEADBEEF37E636E6CA11EDEADBEEFCA11ED",
-    }
+    concrete_transactions = []
 
-    concrete_transactions = {}
-    creation_tx_ids = []
-    tx_constraints = constraints.copy()
-    minimize = []
+    tx_constraints, minimize = _set_minimisation_constraints(
+        transaction_sequence, constraints.copy(), [], 5000
+    )
+    model = get_model(tx_constraints, minimize=minimize)
 
-    transactions = []
+    min_price_dict = {}  # type: Dict[str, int]
     for transaction in transaction_sequence:
-        tx_id = str(transaction.id)
-        if not isinstance(transaction, ContractCreationTransaction):
-            transactions.append(transaction)
-            # Constrain calldatasize
-            max_calldatasize = symbol_factory.BitVecVal(5000, 256)
-            tx_constraints.append(
-                UGE(max_calldatasize, transaction.call_data.calldatasize)
-            )
+        concrete_transaction = _get_concrete_transaction(model, transaction)
+        concrete_transactions.append(concrete_transaction)
+
+        caller = concrete_transaction["origin"]
+        value = int(concrete_transaction["value"], 16)
+        min_price_dict[caller] = min_price_dict.get(caller, 0) + value
+
+    if isinstance(transaction_sequence[0], ContractCreationTransaction):
+        initial_accounts = transaction_sequence[0].prev_world_state.accounts
+    else:
+        initial_accounts = transaction_sequence[0].world_state.accounts
+
+    concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict)
+
+    steps = {"initialState": concrete_initial_state, "steps": concrete_transactions}
+
+    return steps
+
+
+def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
+    """ Gets a concrete state """
+    accounts = {}
+    for address, account in initial_accounts.items():
+        # Skip empty default account
+
+        data = dict()  # type: Dict[str, Union[int, str]]
+        data["nonce"] = account.nonce
+        data["code"] = account.code.bytecode
+        data["storage"] = str(account.storage)
+        data["balance"] = min_price_dict.get(address, 0)
+        accounts[hex(address)] = data
+    return accounts
+
+
+def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
+    """ Gets a concrete transaction from a transaction and z3 model"""
+    # Get concrete values from transaction
+    address = hex(transaction.callee_account.address.value)
+    value = model.eval(transaction.call_value.raw, model_completion=True).as_long()
+    caller = "0x" + (
+        "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
+    ).zfill(40)
+
+    if isinstance(transaction, ContractCreationTransaction):
+        address = ""
+        input_ = transaction.code.bytecode
+    else:
+        input_ = "".join(
+            [
+                hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
+                for b in transaction.call_data.concrete(model)
+            ]
+        )
 
-            minimize.append(transaction.call_data.calldatasize)
-            minimize.append(transaction.call_value)
+    # Create concrete transaction dict
+    concrete_transaction = dict()  # type: Dict[str, str]
+    concrete_transaction["input"] = "0x" + input_
+    concrete_transaction["value"] = "0x%x" % value
+    # Fixme: base origin assignment on origin symbol
+    concrete_transaction["origin"] = caller
+    concrete_transaction["address"] = "%s" % address
 
-            concrete_transactions[tx_id] = tx_template.copy()
+    return concrete_transaction
 
-        else:
-            creation_tx_ids.append(tx_id)
 
-    model = get_model(tx_constraints, minimize=minimize)
+def _set_minimisation_constraints(
+    transaction_sequence, constraints, minimize, max_size
+):
+    """ Set constraints that minimise key transaction values
 
-    for transaction in transactions:
-        tx_id = str(transaction.id)
+    Constraints generated:
+    - Upper bound on calldata size
+    - Minimisation of call value's and calldata sizes
 
-        concrete_transactions[tx_id]["calldata"] = "0x" + "".join(
-            [
-                hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
-                for b in transaction.call_data.concrete(model)
-            ]
-        )
+    :param transaction_sequence: Transaction for which the constraints should be applied
+    :param constraints: The constraints array which should contain any added constraints
+    :param minimize: The minimisation array which should contain any variables that should be minimised
+    :param max_size: The max size of the calldata array
+    :return: updated constraints, minimize
+    """
+    for transaction in transaction_sequence:
+        # Set upper bound on calldata size
+        max_calldata_size = symbol_factory.BitVecVal(max_size, 256)
+        constraints.append(UGE(max_calldata_size, transaction.call_data.calldatasize))
 
-        concrete_transactions[tx_id]["call_value"] = (
-            "0x%x"
-            % model.eval(transaction.call_value.raw, model_completion=True).as_long()
-        )
-        concrete_transactions[tx_id]["caller"] = "0x" + (
-            "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
-        ).zfill(40)
+        # Minimize
+        minimize.append(transaction.call_data.calldatasize)
+        minimize.append(transaction.call_value)
 
-    return concrete_transactions
+    return constraints, minimize

mythril/analysis/symbolic.py

@@ -16,6 +16,16 @@ from mythril.laser.ethereum.strategy.basic import (
     ReturnWeightedRandomStrategy,
     BasicSearchStrategy,
 )
+
+from mythril.laser.ethereum.transaction.symbolic import (
+    ATTACKER_ADDRESS,
+    CREATOR_ADDRESS,
+)
+
+
+from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
+from mythril.laser.ethereum.plugins.plugin_loader import LaserPluginLoader
+
 from mythril.laser.ethereum.strategy.extensions.bounded_loops import (
     BoundedLoopsStrategy,
 )
@@ -77,9 +87,23 @@ class SymExecWrapper:
         else:
             raise ValueError("Invalid strategy argument supplied")
 
+        creator_account = Account(
+            hex(CREATOR_ADDRESS), "", dynamic_loader=dynloader, contract_name=None
+        )
+        attacker_account = Account(
+            hex(ATTACKER_ADDRESS), "", dynamic_loader=dynloader, contract_name=None
+        )
+
         requires_statespace = (
             compulsory_statespace or len(get_detection_modules("post", modules)) > 0
         )
+        if not contract.creation_code:
+            self.accounts = {hex(ATTACKER_ADDRESS): attacker_account}
+        else:
+            self.accounts = {
+                hex(CREATOR_ADDRESS): creator_account,
+                hex(ATTACKER_ADDRESS): attacker_account,
+            }
 
         self.laser = svm.LaserEVM(
             dynamic_loader=dynloader,
@@ -102,6 +126,10 @@ class SymExecWrapper:
         if not disable_dependency_pruning:
             plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
 
+        world_state = WorldState()
+        for account in self.accounts.values():
+            world_state.put_account(account)
+
         if run_analysis_modules:
             self.laser.register_hooks(
                 hook_type="pre",
@@ -114,11 +142,15 @@ class SymExecWrapper:
 
         if isinstance(contract, SolidityContract):
             self.laser.sym_exec(
-                creation_code=contract.creation_code, contract_name=contract.name
+                creation_code=contract.creation_code,
+                contract_name=contract.name,
+                world_state=world_state,
             )
         elif isinstance(contract, EVMContract) and contract.creation_code:
             self.laser.sym_exec(
-                creation_code=contract.creation_code, contract_name=contract.name
+                creation_code=contract.creation_code,
+                contract_name=contract.name,
+                world_state=world_state,
             )
         else:
             account = Account(
@@ -128,7 +160,6 @@ class SymExecWrapper:
                 contract_name=contract.name,
                 concrete_storage=False,
             )
-            world_state = WorldState()
             world_state.put_account(account)
             self.laser.sym_exec(world_state=world_state, target_address=address.value)
 

mythril/analysis/templates/report_as_markdown.jinja2

@@ -24,11 +24,11 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 {{ issue.code }}
 ```
 {% endif %}
-{% if verbose and issue.debug %}
+{% if verbose and issue.tx_sequence %}
 --------------------
 ### Debugging Information:
 
-{{ issue.debug }}
+{{ issue.tx_sequence }}
 
 {% endif %}
 {% endfor %}

mythril/analysis/templates/report_as_text.jinja2

@@ -18,11 +18,11 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 
 --------------------
 {% endif %}
-{% if verbose and issue.debug %}
+{% if verbose and issue.tx_sequence %}
 --------------------
 Transaction Sequence:
 
-{{ issue.debug }}
+{{ issue.tx_sequence }}
 {% endif %}
 
 {% endfor %}

mythril/laser/ethereum/instructions.py

@@ -768,9 +768,7 @@ class Instruction:
             size_sym = True
 
         if size_sym:
-            size = (
-                320
-            )  # This excess stuff will get overwritten as memory is dynamically sized
+            size = 320  # The excess size will get overwritten
 
         size = cast(int, size)
         if size > 0:
@@ -1381,15 +1379,7 @@ class Instruction:
                 return self._sload_helper(global_state, str(index))
 
             storage_keys = global_state.environment.active_account.storage.keys()
-            keys = filter(keccak_function_manager.is_keccak, storage_keys)
-            addr = global_state.get_current_instruction()["address"]
-            keccak_keys = [
-                key
-                for key in keys
-                if global_state.environment.active_account.storage.potential_func(
-                    key, addr
-                )
-            ]
+            keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
 
             results = []  # type: List[GlobalState]
             constraints = []
@@ -1427,16 +1417,11 @@ class Instruction:
         :param constraints:
         :return:
         """
-        address = global_state.get_current_instruction()["address"]
         try:
-            data = global_state.environment.active_account.storage.get(
-                index, addr=address
-            )
+            data = global_state.environment.active_account.storage[index]
         except KeyError:
             data = global_state.new_bitvec("storage_" + str(index), 256)
-            global_state.environment.active_account.storage.put(
-                key=index, value=data, addr=address
-            )
+            global_state.environment.active_account.storage[index] = data
 
         if constraints is not None:
             global_state.mstate.constraints += constraints
@@ -1480,15 +1465,7 @@ class Instruction:
                 return self._sstore_helper(global_state, str(index), value)
 
             storage_keys = global_state.environment.active_account.storage.keys()
-            keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
-            addr = global_state.get_current_instruction()["address"]
-            keccak_keys = [
-                key
-                for key in keccak_keys
-                if global_state.environment.active_account.storage.potential_func(
-                    key, addr
-                )
-            ]
+            keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
 
             results = []  # type: List[GlobalState]
             new = symbol_factory.Bool(False)
@@ -1541,18 +1518,19 @@ class Instruction:
         :param constraint:
         :return:
         """
-        global_state.environment.active_account = deepcopy(
-            global_state.environment.active_account
-        )
-        global_state.accounts[
-            global_state.environment.active_account.address.value
-        ] = global_state.environment.active_account
-        address = global_state.get_current_instruction()["address"]
-        global_state.environment.active_account.storage.put(
-            key=index,
-            value=value if not isinstance(value, Expression) else simplify(value),
-            addr=address,
-        )
+        try:
+            global_state.environment.active_account = deepcopy(
+                global_state.environment.active_account
+            )
+            global_state.accounts[
+                global_state.environment.active_account.address.value
+            ] = global_state.environment.active_account
+
+            global_state.environment.active_account.storage[index] = (
+                value if not isinstance(value, Expression) else simplify(value)
+            )
+        except KeyError:
+            log.debug("Error writing to storage: Invalid index")
 
         if constraint is not None:
             global_state.mstate.constraints.append(constraint)
@@ -1864,6 +1842,14 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader, True
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -1881,7 +1867,6 @@ class Instruction:
         )
         if native_result:
             return native_result
-
         transaction = MessageCallTransaction(
             world_state=global_state.world_state,
             gas_price=environment.gasprice,

mythril/laser/ethereum/state/account.py

@@ -24,12 +24,8 @@ class Storage:
         self.concrete = concrete
         self.dynld = dynamic_loader
         self.address = address
-        self._storage_opcodes = {}  # type: Dict
 
-    def get(self, item: Union[str, int], addr: int) -> Any:
-        if item not in self._storage_opcodes:
-            self._storage_opcodes[item] = set()
-        self._storage_opcodes[item].add(addr)
+    def __getitem__(self, item: Union[str, int]) -> Any:
         try:
             return self._storage[item]
         except KeyError:
@@ -60,17 +56,9 @@ class Storage:
         )
         return self._storage[item]
 
-    def put(self, key: Union[int, str], value: Any, addr) -> None:
-        if key not in self._storage_opcodes:
-            self._storage_opcodes[key] = set()
-        self._storage_opcodes[key].add(addr)
+    def __setitem__(self, key: Union[int, str], value: Any) -> None:
         self._storage[key] = value
 
-    def potential_func(self, key, opcode) -> bool:
-        if key not in self._storage_opcodes:
-            return False
-        return opcode in self._storage_opcodes[key]
-
     def keys(self) -> KeysView:
         """
 
@@ -85,6 +73,9 @@ class Storage:
         storage._storage = copy(self._storage)
         return storage
 
+    def __str__(self):
+        return str(self._storage)
+
 
 class Account:
     """Account class representing ethereum accounts."""

mythril/laser/ethereum/svm.py

@@ -69,6 +69,7 @@ class LaserEVM:
         :param enable_iprof: Variable indicating whether instruction profiling should be turned on
         """
         self.open_states = []  # type: List[WorldState]
+
         self.total_states = 0
         self.dynamic_loader = dynamic_loader
 
@@ -125,7 +126,7 @@ class LaserEVM:
         :param creation_code The creation code to create the target contract in the symbolic environment
         :param contract_name The name that the created account should be associated with
         """
-        pre_configuration_mode = world_state is not None and target_address is not None
+        pre_configuration_mode = target_address is not None
         scratch_mode = creation_code is not None and contract_name is not None
         if pre_configuration_mode == scratch_mode:
             raise ValueError("Symbolic execution started with invalid parameters")
@@ -144,14 +145,16 @@ class LaserEVM:
 
         elif scratch_mode:
             log.info("Starting contract creation transaction")
+
             created_account = execute_contract_creation(
-                self, creation_code, contract_name
+                self, creation_code, contract_name, world_state=world_state
             )
             log.info(
                 "Finished contract creation, found {} open states".format(
                     len(self.open_states)
                 )
             )
+
             if len(self.open_states) == 0:
                 log.warning(
                     "No contract was created during the execution of contract creation "

mythril/laser/ethereum/transaction/symbolic.py

@@ -68,7 +68,7 @@ def execute_message_call(laser_evm, callee_address: BitVec) -> None:
 
 
 def execute_contract_creation(
-    laser_evm, contract_initialization_code, contract_name=None
+    laser_evm, contract_initialization_code, contract_name=None, world_state=None
 ) -> Account:
     """Executes a contract creation transaction from all open states.
 
@@ -80,15 +80,9 @@ def execute_contract_creation(
     # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
     del laser_evm.open_states[:]
 
-    world_state = WorldState()
+    world_state = world_state or WorldState()
     open_states = [world_state]
-    new_account = world_state.create_account(
-        0, concrete_storage=True, dynamic_loader=None, creator=CREATOR_ADDRESS
-    )
-
-    if contract_name:
-        new_account.contract_name = contract_name
-
+    new_account = None
     for open_world_state in open_states:
         next_transaction_id = get_next_transaction_id()
         transaction = ContractCreationTransaction(
@@ -103,13 +97,14 @@ def execute_contract_creation(
             ),
             code=Disassembly(contract_initialization_code),
             caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256),
-            callee_account=new_account,
+            contract_name=contract_name,
             call_data=[],
             call_value=symbol_factory.BitVecSym(
                 "call_value{}".format(next_transaction_id), 256
             ),
         )
         _setup_global_state_for_execution(laser_evm, transaction)
+        new_account = new_account or transaction.callee_account
     laser_evm.exec(True)
 
     return new_account

mythril/laser/ethereum/transaction/transaction_models.py

@@ -2,6 +2,7 @@
 execution."""
 
 import array
+from copy import deepcopy
 from z3 import ExprRef
 from typing import Union, Optional, cast
 
@@ -161,12 +162,37 @@ class MessageCallTransaction(BaseTransaction):
 class ContractCreationTransaction(BaseTransaction):
     """Transaction object models an transaction."""
 
-    def __init__(self, *args, **kwargs) -> None:
-        # Remove ignore after https://github.com/python/mypy/issues/4335 is fixed
-        super().__init__(*args, **kwargs, init_call_data=False)  # type: ignore
+    def __init__(
+        self,
+        world_state: WorldState,
+        caller: ExprRef = None,
+        call_data=None,
+        identifier: Optional[str] = None,
+        gas_price=None,
+        gas_limit=None,
+        origin=None,
+        code=None,
+        call_value=None,
+        contract_name=None,
+    ) -> None:
+        self.prev_world_state = deepcopy(world_state)
+        callee_account = world_state.create_account(
+            0, concrete_storage=True, creator=caller.value
+        )
+        callee_account.contract_name = contract_name
         # TODO: set correct balance for new account
-        self.callee_account = self.callee_account or self.world_state.create_account(
-            0, concrete_storage=True
+        super().__init__(
+            world_state=world_state,
+            callee_account=callee_account,
+            caller=caller,
+            call_data=call_data,
+            identifier=identifier,
+            gas_price=gas_price,
+            gas_limit=gas_limit,
+            origin=origin,
+            code=code,
+            call_value=call_value,
+            init_call_data=False,
         )
 
     def initial_global_state(self) -> GlobalState:

mythril/laser/smt/bitvec.py

@@ -243,6 +243,13 @@ class BitVec(Expression[z3.BitVecRef]):
         """
         return self._handle_shift(other, rshift)
 
+    def __hash__(self) -> int:
+        """
+
+        :return:
+        """
+        return self.raw.__hash__()
+
 
 def _comparison_helper(
     a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool

tests/laser/evm_testsuite/evm_test.py

@@ -125,7 +125,7 @@ def test_vmtest(
         account.code = Disassembly(details["code"][2:])
         account.nonce = int(details["nonce"], 16)
         for key, value in details["storage"].items():
-            account.storage.put(int(key, 16), int(value, 16), 10)
+            account.storage[int(key, 16)] = int(value, 16)
 
         world_state.put_account(account)
         account.set_balance(int(details["balance"], 16))
@@ -175,7 +175,7 @@ def test_vmtest(
 
             for index, value in details["storage"].items():
                 expected = int(value, 16)
-                actual = account.storage.get(int(index, 16), 0)
+                actual = account.storage[int(index, 16)]
 
                 if isinstance(actual, Expression):
                     actual = actual.value

tests/laser/state/storage_test.py

@@ -12,7 +12,7 @@ def test_concrete_storage_uninitialized_index(initial_storage, key):
     storage._storage = initial_storage
 
     # Act
-    value = storage.get(key, 0)
+    value = storage[key]
 
     # Assert
     assert value == 0
@@ -25,7 +25,7 @@ def test_symbolic_storage_uninitialized_index(initial_storage, key):
     storage._storage = initial_storage
 
     # Act
-    value = storage.get(key, 0)
+    value = storage[key]
 
     # Assert
     assert isinstance(value, Expression)
@@ -36,10 +36,10 @@ def test_storage_set_item():
     storage = Storage()
 
     # Act
-    storage.put(key=1, value=13, addr=10)
+    storage[1] = 13
 
     # Assert
-    assert storage.get(item=1, addr=10) == 13
+    assert storage[1] == 13
 
 
 def test_storage_change_item():
@@ -47,7 +47,7 @@ def test_storage_change_item():
     storage = Storage()
     storage._storage = {1: 12}
     # Act
-    storage.put(key=1, value=14, addr=10)
+    storage[1] = 14
 
     # Assert
-    assert storage.get(item=1, addr=10) == 14
+    assert storage[1] == 14

tests/report_test.py

@@ -17,7 +17,8 @@ def _fix_path(text):
 def _fix_debug_data(json_str):
     read_json = json.loads(json_str)
     for issue in read_json["issues"]:
-        issue["debug"] = "<DEBUG-DATA>"
+        issue["tx_sequence"] = "<TX-DATA>"
+
     return json.dumps(read_json, sort_keys=True, indent=4)
 
 
@@ -25,6 +26,7 @@ def _add_jsonv2_stubs(json_str):
     read_json = json.loads(json_str)
     for issue in read_json[0]["issues"]:
         issue["extra"]["discoveryTime"] = "<DISCOVERY-TIME-DATA>"
+        issue["extra"]["testCase"] = "<TEST-CASE>"
     return json.dumps(read_json, sort_keys=True, indent=4)
 
 

tests/testdata/outputs_expected/calls.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 661,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "thisisfine()",
             "max_gas_used": 1254,
@@ -12,12 +11,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To User-Supplied Address"
+            "title": "External Call To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 661,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "thisisfine()",
             "max_gas_used": 35972,
@@ -25,12 +24,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 779,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "callstoredaddress()",
             "max_gas_used": 1298,
@@ -38,12 +37,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To User-Supplied Address"
+            "title": "External Call To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 779,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "callstoredaddress()",
             "max_gas_used": 36016,
@@ -51,12 +50,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 858,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "reentrancy()",
             "max_gas_used": 1320,
@@ -64,12 +63,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To User-Supplied Address"
+            "title": "External Call To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 858,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "reentrancy()",
             "max_gas_used": 61052,
@@ -77,12 +76,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 869,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The contract account state is changed after an external call. \nConsider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.",
             "function": "reentrancy()",
             "max_gas_used": null,
@@ -90,12 +89,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "State change after external call"
+            "title": "State change after external call",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 912,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "calluseraddress(address)",
             "max_gas_used": 616,
@@ -103,12 +102,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To User-Supplied Address"
+            "title": "External Call To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 912,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "calluseraddress(address)",
             "max_gas_used": 35336,
@@ -116,7 +115,8 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/calls.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -24,7 +25,8 @@
                     "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -41,7 +43,8 @@
                     "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -58,7 +61,8 @@
                     "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -75,7 +79,8 @@
                     "tail": "Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -92,7 +97,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -109,7 +115,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -126,7 +133,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -143,7 +151,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/ether_send.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 722,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "Anyone can withdraw ETH from the contract account.\nArbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.",
             "function": "withdrawfunds()",
             "max_gas_used": 1749,
@@ -12,12 +11,12 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "105",
-            "title": "Unprotected Ether Withdrawal"
+            "title": "Unprotected Ether Withdrawal",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 883,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
             "function": "invest()",
             "max_gas_used": 26883,
@@ -25,7 +24,8 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
-            "title": "Integer Overflow"
+            "title": "Integer Overflow",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/ether_send.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -24,7 +25,8 @@
                     "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/exceptions.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 446,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
             "function": "assert3(uint256)",
             "max_gas_used": 301,
@@ -12,12 +11,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "110",
-            "title": "Exception State"
+            "title": "Exception State",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 484,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
             "function": "arrayaccess(uint256)",
             "max_gas_used": 351,
@@ -25,12 +24,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "110",
-            "title": "Exception State"
+            "title": "Exception State",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 506,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
             "function": "divisionby0(uint256)",
             "max_gas_used": 367,
@@ -38,12 +37,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "110",
-            "title": "Exception State"
+            "title": "Exception State",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 531,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
             "function": "assert1()",
             "max_gas_used": 363,
@@ -51,7 +50,8 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "110",
-            "title": "Exception State"
+            "title": "Exception State",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/exceptions.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -24,7 +25,8 @@
                     "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -41,7 +43,8 @@
                     "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -58,7 +61,8 @@
                     "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/kinds_of_calls.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 618,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "_function_0x141f32ff",
             "max_gas_used": 35865,
@@ -12,12 +11,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 618,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "Use of callcode is deprecated.\nThe callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead.",
             "function": "_function_0x141f32ff",
             "max_gas_used": 1141,
@@ -25,12 +24,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "111",
-            "title": "Use of callcode"
+            "title": "Use of callcode",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 849,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The contract delegates execution to another contract with a user-supplied address.\nThe smart contract delegates execution to a user-supplied address. Note that callers can execute arbitrary contracts and that the callee contract can access the storage of the calling contract. ",
             "function": "_function_0x9b58bc26",
             "max_gas_used": 35928,
@@ -38,12 +37,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "112",
-            "title": "Delegatecall Proxy To User-Supplied Address"
+            "title": "Delegatecall Proxy To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 849,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "_function_0x9b58bc26",
             "max_gas_used": 35928,
@@ -51,12 +50,12 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 1038,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "_function_0xeea4c864",
             "max_gas_used": 1229,
@@ -64,12 +63,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To User-Supplied Address"
+            "title": "External Call To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 1038,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "_function_0xeea4c864",
             "max_gas_used": 35953,
@@ -77,7 +76,8 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/kinds_of_calls.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "The smart contract delegates execution to a user-supplied address. Note that callers can execute arbitrary contracts and that the callee contract can access the storage of the calling contract. "
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -24,7 +25,8 @@
                     "tail": "The callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -41,7 +43,8 @@
                     "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -58,7 +61,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -75,7 +79,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -92,7 +97,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/metacoin.sol.o.json

@@ -1,19 +1,5 @@
 {
     "error": null,
-    "issues": [
-        {
-            "address": 498,
-            "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
-            "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
-            "function": "sendToken(address,uint256)",
-            "max_gas_used": 52806,
-            "min_gas_used": 11860,
-            "severity": "High",
-            "sourceMap": null,
-            "swc-id": "101",
-            "title": "Integer Overflow"
-        }
-    ],
+    "issues": [],
     "success": true
 }

tests/testdata/outputs_expected/metacoin.sol.o.jsonv2

@@ -1,24 +1,6 @@
 [
     {
-        "issues": [
-            {
-                "description": {
-                    "head": "The binary addition can overflow.",
-                    "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
-                },
-                "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
-                },
-                "locations": [
-                    {
-                        "sourceMap": "498:1:0"
-                    }
-                ],
-                "severity": "High",
-                "swcID": "SWC-101",
-                "swcTitle": "Integer Overflow and Underflow"
-            }
-        ],
+        "issues": [],
         "meta": {},
         "sourceFormat": "evm-byzantium-bytecode",
         "sourceList": [

tests/testdata/outputs_expected/metacoin.sol.o.markdown

@@ -1,14 +1,3 @@
-# Analysis results for test-filename.sol
+# Analysis results for None
 
-## Integer Overflow
-- SWC ID: 101
-- Severity: High
-- Contract: Unknown
-- Function name: `sendToken(address,uint256)`
-- PC address: 498
-- Estimated Gas Usage: 11860 - 52806
-
-### Description
-
-The binary addition can overflow.
-The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.
+The analysis was completed successfully. No issues were detected.

tests/testdata/outputs_expected/metacoin.sol.o.text

@@ -1,11 +1 @@
-==== Integer Overflow ====
-SWC ID: 101
-Severity: High
-Contract: Unknown
-Function name: sendToken(address,uint256)
-PC address: 498
-Estimated Gas Usage: 11860 - 52806
-The binary addition can overflow.
-The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.
---------------------
-
+The analysis was completed successfully. No issues were detected.

tests/testdata/outputs_expected/multi_contracts.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 142,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "Anyone can withdraw ETH from the contract account.\nArbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.",
             "function": "transfer()",
             "max_gas_used": 467,
@@ -12,7 +11,8 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "105",
-            "title": "Unprotected Ether Withdrawal"
+            "title": "Unprotected Ether Withdrawal",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/multi_contracts.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/origin.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 317,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "Use of tx.origin is deprecated.\nThe smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the  future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin",
             "function": "transferOwnership(address)",
             "max_gas_used": 1051,
@@ -12,7 +11,8 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "111",
-            "title": "Use of tx.origin"
+            "title": "Use of tx.origin",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/origin.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "The smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the  future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin"
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/overflow.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 567,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
             "max_gas_used": 78155,
@@ -12,12 +11,12 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
-            "title": "Integer Underflow"
+            "title": "Integer Underflow",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 649,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
             "max_gas_used": 78155,
@@ -25,12 +24,12 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
-            "title": "Integer Underflow"
+            "title": "Integer Underflow",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 725,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
             "max_gas_used": 78155,
@@ -38,7 +37,8 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
-            "title": "Integer Overflow"
+            "title": "Integer Overflow",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/overflow.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -24,7 +25,8 @@
                     "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -41,7 +43,8 @@
                     "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/returnvalue.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 196,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "callchecked()",
             "max_gas_used": 1210,
@@ -12,12 +11,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To User-Supplied Address"
+            "title": "External Call To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 285,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "callnotchecked()",
             "max_gas_used": 1232,
@@ -25,12 +24,12 @@
             "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To User-Supplied Address"
+            "title": "External Call To User-Supplied Address",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 285,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
             "function": "callnotchecked()",
             "max_gas_used": 35950,
@@ -38,7 +37,8 @@
             "severity": "Low",
             "sourceMap": null,
             "swc-id": "104",
-            "title": "Unchecked Call Return Value"
+            "title": "Unchecked Call Return Value",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/returnvalue.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -24,7 +25,8 @@
                     "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -41,7 +43,8 @@
                     "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/suicide.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 146,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The contract can be killed by anyone.\nAnyone can kill this contract and withdraw its balance to an arbitrary address.",
             "function": "kill(address)",
             "max_gas_used": 263,
@@ -12,7 +11,8 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "106",
-            "title": "Unprotected Selfdestruct"
+            "title": "Unprotected Selfdestruct",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/suicide.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "Anyone can kill this contract and withdraw its balance to an arbitrary address."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {

tests/testdata/outputs_expected/underflow.sol.o.json

@@ -4,7 +4,6 @@
         {
             "address": 567,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
             "max_gas_used": 52861,
@@ -12,12 +11,12 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
-            "title": "Integer Underflow"
+            "title": "Integer Underflow",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 649,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
             "max_gas_used": 52861,
@@ -25,12 +24,12 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
-            "title": "Integer Underflow"
+            "title": "Integer Underflow",
+            "tx_sequence": "<TX-DATA>"
         },
         {
             "address": 725,
             "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
             "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
             "max_gas_used": 52861,
@@ -38,7 +37,8 @@
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
-            "title": "Integer Overflow"
+            "title": "Integer Overflow",
+            "tx_sequence": "<TX-DATA>"
         }
     ],
     "success": true

tests/testdata/outputs_expected/underflow.sol.o.jsonv2

@@ -7,7 +7,8 @@
                     "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -24,7 +25,8 @@
                     "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {
@@ -41,7 +43,8 @@
                     "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
                 },
                 "extra": {
-                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>",
+                    "testCase": "<TEST-CASE>"
                 },
                 "locations": [
                     {