Merge branch 'develop' into memory_refactor

mythril/analysis/analysis_utils.py

@@ -1,48 +0,0 @@
-import re
-from typing import List
-from z3 import *
-from mythril.laser.ethereum.transaction import ContractCreationTransaction
-from mythril.laser.ethereum.state.global_state import GlobalState
-
-
-def get_non_creator_constraints(state: GlobalState) -> (List, bool):
-    """
-    Get constraints which say that the caller isn't the creator of the contract
-    :param state: The state
-    :return: tuple of (constraints, bool) where the bool says whether the caller is constrained or not
-    """
-    not_creator_constraints = []
-    creator = None
-    if isinstance(
-        state.world_state.transaction_sequence[0], ContractCreationTransaction
-    ):
-        creator = state.world_state.transaction_sequence[0].caller
-
-    if creator is not None:
-        for transaction in state.world_state.transaction_sequence[1:]:
-            not_creator_constraints.append(
-                Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))
-            )
-            not_creator_constraints.append(
-                Not(Extract(159, 0, transaction.caller) == 0)
-            )
-    else:
-        for transaction in state.world_state.transaction_sequence:
-            not_creator_constraints.append(
-                Not(Extract(159, 0, transaction.caller) == 0)
-            )
-        if not has_caller_check_constraint(state.mstate.constraints):
-            return [], True
-    return not_creator_constraints, False
-
-
-def has_caller_check_constraint(constraints: List) -> bool:
-    """
-    Checks whether the caller is constrained to a value or not
-    """
-    for constraint in constraints:
-        if re.search(
-            r"caller.*==[0-9]{20}", str(constraint).replace("\n", "").replace(" ", "")
-        ):
-            return False
-    return True

mythril/analysis/modules/delegatecall.py

@@ -37,9 +37,6 @@ class DelegateCallModule(DetectionModule):
             if meminstart.type == VarType.CONCRETE:
                 issues += self._concrete_call(call, state, address, meminstart)
 
-            if call.to.type == VarType.SYMBOLIC:
-                issues += self._symbolic_call(call, state, address, statespace)
-
         return issues
 
     def _concrete_call(self, call, state, address, meminstart):
@@ -68,45 +65,5 @@ class DelegateCallModule(DetectionModule):
 
         return [issue]
 
-    def _symbolic_call(self, call, state, address, statespace):
-        issue = Issue(
-            contract=call.node.contract_name,
-            function_name=call.node.function_name,
-            address=address,
-            swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
-            bytecode=state.environment.code.bytecode,
-            title=call.type + " to a user-supplied address",
-            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
-        )
-
-        if "calldata" in str(call.to):
-            issue.description = "This contract delegates execution to a contract address obtained from calldata."
-
-        else:
-            m = re.search(r"storage_([a-z0-9_&^]+)", str(call.to))
-
-            if m:
-                idx = m.group(1)
-                func = statespace.find_storage_write(
-                    state.environment.active_account.address, idx
-                )
-
-                if func:
-                    issue.description = (
-                        "This contract delegates execution to a contract address in storage slot "
-                        + str(idx)
-                        + ". This storage slot can be written to by calling the function `"
-                        + func
-                        + "`."
-                    )
-
-                else:
-                    logging.debug(
-                        "[DELEGATECALL] No storage writes to index " + str(idx)
-                    )
-
-        issue.description += " Be aware that the called contract gets unrestricted access to this contract's state."
-        return [issue]
-
 
 detector = DelegateCallModule()

mythril/analysis/modules/ether_thief.py

@@ -1,13 +1,13 @@
 from mythril.analysis.ops import *
 from mythril.analysis import solver
-from mythril.analysis.analysis_utils import get_non_creator_constraints
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.analysis.modules.base import DetectionModule
+from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.exceptions import UnsatError
-from z3 import BitVecVal, UGT
+from z3 import BitVecVal, UGT, Sum
 import logging
-
+from copy import copy
 
 DESCRIPTION = """
 
@@ -22,7 +22,56 @@ An issue is reported if:
 
 """
 
-ARBITRARY_SENDER_ADDRESS = 0xAAAAAAAABBBBBBBBBCCCCCCCDDDDDDDDEEEEEEEE
+
+def _analyze_state(state):
+    instruction = state.get_current_instruction()
+    node = state.node
+
+    if instruction["opcode"] != "CALL":
+        return []
+
+    call_value = state.mstate.stack[-3]
+    target = state.mstate.stack[-2]
+
+    eth_sent_total = BitVecVal(0, 256)
+
+    constraints = copy(node.constraints)
+
+    for tx in state.world_state.transaction_sequence:
+        if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF:
+
+            # There's sometimes no overflow check on balances added.
+            # But we don't care about attacks that require more 2^^256 ETH to be sent.
+
+            constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)]
+            eth_sent_total = Sum(eth_sent_total, tx.call_value)
+    constraints += [UGT(call_value, eth_sent_total), target == state.environment.sender]
+
+    try:
+
+        transaction_sequence = solver.get_transaction_sequence(state, constraints)
+
+        debug = str(transaction_sequence)
+
+        issue = Issue(
+            contract=node.contract_name,
+            function_name=node.function_name,
+            address=instruction["address"],
+            swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
+            title="Ether thief",
+            _type="Warning",
+            bytecode=state.environment.code.bytecode,
+            description="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,
+            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+        )
+    except UnsatError:
+        logging.debug("[ETHER_THIEF] no model found")
+        return []
+
+    return [issue]
 
 
 class EtherThief(DetectionModule):
@@ -32,73 +81,17 @@ class EtherThief(DetectionModule):
             swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
             hooks=["CALL"],
             description=DESCRIPTION,
+            entrypoint="callback",
         )
+        self._issues = []
+
+    def execute(self, state: GlobalState):
+        self._issues.extend(_analyze_state(state))
+        return self.issues
 
-    def execute(self, state_space):
-        logging.debug("Executing module: %s", self.name)
-        issues = []
-
-        for k in state_space.nodes:
-            node = state_space.nodes[k]
-            for state in node.states:
-                issues += self._analyze_state(state, node)
-
-        return issues
-
-    @staticmethod
-    def _analyze_state(state, node):
-        issues = []
-        instruction = state.get_current_instruction()
-
-        if instruction["opcode"] != "CALL":
-            return []
-
-        call_value = state.mstate.stack[-3]
-        target = state.mstate.stack[-2]
-
-        not_creator_constraints, constrained = get_non_creator_constraints(state)
-        if constrained:
-            return []
-
-        eth_sent_total = BitVecVal(0, 256)
-
-        for tx in state.world_state.transaction_sequence[1:]:
-            eth_sent_total += tx.call_value
-
-        try:
-
-            transaction_sequence = solver.get_transaction_sequence(
-                state,
-                node.constraints
-                + not_creator_constraints
-                + [
-                    UGT(call_value, eth_sent_total),
-                    state.environment.sender == ARBITRARY_SENDER_ADDRESS,
-                    target == state.environment.sender,
-                ],
-            )
-
-            debug = str(transaction_sequence)
-
-            issue = Issue(
-                contract=node.contract_name,
-                function_name=node.function_name,
-                address=instruction["address"],
-                swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
-                title="Ether thief",
-                _type="Warning",
-                bytecode=state.environment.code.bytecode,
-                description="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,
-                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
-            )
-            issues.append(issue)
-        except UnsatError:
-            logging.debug("[ETHER_THIEF] no model found")
-
-        return issues
+    @property
+    def issues(self):
+        return self._issues
 
 
 detector = EtherThief()

mythril/analysis/modules/external_calls.py

@@ -1,218 +1,111 @@
 from z3 import *
-from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.analysis import solver
 from mythril.analysis.swc_data import REENTRANCY
 from mythril.analysis.modules.base import DetectionModule
-import re
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.exceptions import UnsatError
 import logging
-from mythril.laser.ethereum.cfg import JumpType
 
+DESCRIPTION = """
 
-class ExternalCallModule(DetectionModule):
-    def __init__(self, max_search_depth=64):
+Search for low level calls (e.g. call.value()) that forward all gas to the callee.
+Report a warning if the callee address can be set by the sender, otherwise create 
+an informational issue.
+
+"""
+
+
+def _analyze_state(state):
+
+    node = state.node
+    gas = state.mstate.stack[-1]
+    to = state.mstate.stack[-2]
+
+    address = state.get_current_instruction()["address"]
+
+    try:
+        constraints = node.constraints
+        transaction_sequence = solver.get_transaction_sequence(
+            state, constraints + [UGT(gas, 2300)]
+        )
+
+        # Check whether we can also set the callee address
+
+        try:
+            constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF]
+            transaction_sequence = solver.get_transaction_sequence(state, constraints)
+
+            debug = str(transaction_sequence)
+            description = (
+                "The contract executes a function call with high gas to a user-supplied address. "
+                "Note that the callee can contain arbitrary code and may re-enter any function in this contract. "
+                "Review the business logic carefully to prevent unanticipated effects on the contract state."
+            )
+
+            issue = Issue(
+                contract=node.contract_name,
+                function_name=node.function_name,
+                address=address,
+                swc_id=REENTRANCY,
+                title="External call to user-supplied address",
+                _type="Warning",
+                bytecode=state.environment.code.bytecode,
+                description=description,
+                debug=debug,
+                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+            )
+
+        except UnsatError:
+
+            logging.debug(
+                "[EXTERNAL_CALLS] Callee address cannot be modified. Reporting informational issue."
+            )
+
+            debug = str(transaction_sequence)
+            description = (
+                "The contract executes a function call to an external address. "
+                "Verify that the code at this address is trusted and immutable."
+            )
+
+            issue = Issue(
+                contract=node.contract_name,
+                function_name=state.node.function_name,
+                address=address,
+                swc_id=REENTRANCY,
+                title="External call",
+                _type="Informational",
+                bytecode=state.environment.code.bytecode,
+                description=description,
+                debug=debug,
+                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+            )
+
+    except UnsatError:
+        logging.debug("[EXTERNAL_CALLS] No model found.")
+        return []
+
+    return [issue]
+
+
+class ExternalCalls(DetectionModule):
+    def __init__(self):
         super().__init__(
-            name="External Calls",
+            name="External calls",
             swc_id=REENTRANCY,
             hooks=["CALL"],
-            description="Check for call.value()() to external addresses",
+            description=(DESCRIPTION),
+            entrypoint="callback",
         )
-        self.max_search_depth = max_search_depth
-        self.calls_visited = []
-
-    def search_children(
-        self, statespace, node, transaction_id, start_index=0, depth=0, results=None
-    ):
-        if results is None:
-            results = []
-        logging.debug("SEARCHING NODE %d", node.uid)
-
-        if depth < self.max_search_depth:
-
-            n_states = len(node.states)
-
-            if n_states > start_index:
-
-                for j in range(start_index, n_states):
-                    if (
-                        node.states[j].get_current_instruction()["opcode"] == "SSTORE"
-                        and node.states[j].current_transaction.id == transaction_id
-                    ):
-                        results.append(
-                            node.states[j].get_current_instruction()["address"]
-                        )
-            children = []
-
-            for edge in statespace.edges:
-                if edge.node_from == node.uid and edge.type != JumpType.Transaction:
-                    children.append(statespace.nodes[edge.node_to])
-
-            if len(children):
-                for node in children:
-                    results += self.search_children(
-                        statespace,
-                        node,
-                        transaction_id,
-                        depth=depth + 1,
-                        results=results,
-                    )
-
-        return results
-
-    def execute(self, statespace):
-
-        issues = []
-
-        for call in statespace.calls:
-
-            state = call.state
-            address = state.get_current_instruction()["address"]
-
-            if call.type == "CALL":
-
-                logging.debug(
-                    "[EXTERNAL_CALLS] Call to: %s, value = %s, gas = %s"
-                    % (str(call.to), str(call.value), str(call.gas))
-                )
-
-                if (
-                    call.to.type == VarType.SYMBOLIC
-                    and (call.gas.type == VarType.CONCRETE and call.gas.val > 2300)
-                    or (
-                        call.gas.type == VarType.SYMBOLIC
-                        and "2300" not in str(call.gas)
-                    )
-                ):
-
-                    description = "This contract executes a message call to "
-
-                    target = str(call.to)
-                    user_supplied = False
-
-                    if "calldata" in target or "caller" in target:
-
-                        if "calldata" in target:
-                            description += (
-                                "an address provided as a function argument. "
-                            )
-                        else:
-                            description += "the address of the transaction sender. "
-
-                        user_supplied = True
-                    else:
-                        m = re.search(r"storage_([a-z0-9_&^]+)", str(call.to))
-
-                        if m:
-                            idx = m.group(1)
-
-                            func = statespace.find_storage_write(
-                                state.environment.active_account.address, idx
-                            )
-
-                            if func:
-
-                                description += (
-                                    "an address found at storage slot "
-                                    + str(idx)
-                                    + ". "
-                                    + "This storage slot can be written to by calling the function `"
-                                    + func
-                                    + "`. "
-                                )
-                                user_supplied = True
-
-                    if user_supplied:
-
-                        description += (
-                            "Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. "
-                            "Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state."
-                        )
-
-                        issue = Issue(
-                            contract=call.node.contract_name,
-                            function_name=call.node.function_name,
-                            address=address,
-                            title="Message call to external contract",
-                            _type="Warning",
-                            description=description,
-                            bytecode=state.environment.code.bytecode,
-                            swc_id=REENTRANCY,
-                            gas_used=(
-                                state.mstate.min_gas_used,
-                                state.mstate.max_gas_used,
-                            ),
-                        )
-
-                    else:
-
-                        description += "to another contract. Make sure that the called contract is trusted and does not execute user-supplied code."
-
-                        issue = Issue(
-                            contract=call.node.contract_name,
-                            function_name=call.node.function_name,
-                            address=address,
-                            title="Message call to external contract",
-                            _type="Informational",
-                            description=description,
-                            bytecode=state.environment.code.bytecode,
-                            swc_id=REENTRANCY,
-                            gas_used=(
-                                state.mstate.min_gas_used,
-                                state.mstate.max_gas_used,
-                            ),
-                        )
-
-                    issues.append(issue)
-
-                    if address not in self.calls_visited:
-                        self.calls_visited.append(address)
-
-                        logging.debug(
-                            "[EXTERNAL_CALLS] Checking for state changes starting from "
-                            + call.node.function_name
-                        )
-
-                        # Check for SSTORE in remaining instructions in current node & nodes down the CFG
-
-                        state_change_addresses = self.search_children(
-                            statespace,
-                            call.node,
-                            call.state.current_transaction.id,
-                            call.state_index + 1,
-                            depth=0,
-                            results=[],
-                        )
-
-                        logging.debug(
-                            "[EXTERNAL_CALLS] Detected state changes at addresses: "
-                            + str(state_change_addresses)
-                        )
-
-                        if len(state_change_addresses):
-                            for address in state_change_addresses:
-                                description = (
-                                    "The contract account state is changed after an external call. "
-                                    "Consider that the called contract could re-enter the function before this "
-                                    "state change takes place. This can lead to business logic vulnerabilities."
-                                )
-
-                                issue = Issue(
-                                    contract=call.node.contract_name,
-                                    function_name=call.node.function_name,
-                                    address=address,
-                                    title="State change after external call",
-                                    _type="Warning",
-                                    description=description,
-                                    bytecode=state.environment.code.bytecode,
-                                    swc_id=REENTRANCY,
-                                    gas_used=(
-                                        state.mstate.min_gas_used,
-                                        state.mstate.max_gas_used,
-                                    ),
-                                )
-                                issues.append(issue)
-
-        return issues
-
-
-detector = ExternalCallModule()
+        self._issues = []
+
+    def execute(self, state: GlobalState):
+        self._issues.extend(_analyze_state(state))
+        return self.issues
+
+    @property
+    def issues(self):
+        return self._issues
+
+
+detector = ExternalCalls()

mythril/analysis/modules/integer.py

@@ -167,33 +167,19 @@ class IntegerOverflowUnderflowModule(DetectionModule):
 
             constraints = copy.deepcopy(node.constraints)
 
-            # Filter for patterns that indicate benign underflows
-
-            # Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large.
-            # Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0
             if type(op0) == int and type(op1) == int:
                 return []
-            if re.search(r"calldatasize_", str(op0)):
-                return []
-            if re.search(r"256\*.*If\(1", str(op0), re.DOTALL) or re.search(
-                r"256\*.*If\(1", str(op1), re.DOTALL
-            ):
-                return []
-            if re.search(r"32 \+.*calldata", str(op0), re.DOTALL) or re.search(
-                r"32 \+.*calldata", str(op1), re.DOTALL
-            ):
-                return []
 
             logging.debug(
                 "[INTEGER_UNDERFLOW] Checking SUB {0}, {1} at address {2}".format(
                     str(op0), str(op1), str(instruction["address"])
                 )
             )
+
             allowed_types = [int, BitVecRef, BitVecNumRef]
 
             if type(op0) in allowed_types and type(op1) in allowed_types:
-                constraints.append(UGT(op1, op0))
-
+                constraints.append(Not(BVSubNoUnderflow(op0, op1, signed=False)))
                 try:
 
                     model = solver.get_model(constraints)

mythril/analysis/modules/suicide.py

@@ -1,5 +1,4 @@
 from mythril.analysis import solver
-from mythril.analysis.analysis_utils import get_non_creator_constraints
 from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
@@ -13,8 +12,6 @@ Check if the contact can be 'accidentally' killed by anyone.
 For kill-able contracts, also check whether it is possible to direct the contract balance to the attacker.
 """
 
-ARBITRARY_SENDER_ADDRESS = 0xAAAAAAAABBBBBBBBBCCCCCCCDDDDDDDDEEEEEEEE
-
 
 def _analyze_state(state):
     logging.info("Suicide module: Analyzing suicide instruction")
@@ -24,24 +21,17 @@ def _analyze_state(state):
 
     logging.debug("[SUICIDE] SUICIDE in function " + node.function_name)
 
-    not_creator_constraints, constrained = get_non_creator_constraints(state)
-    constraints = (
-        node.constraints
-        + not_creator_constraints
-        + [state.environment.sender == ARBITRARY_SENDER_ADDRESS]
-    )
-
-    if constrained:
-        return []
-
     try:
         try:
             transaction_sequence = solver.get_transaction_sequence(
-                state, constraints + [to == ARBITRARY_SENDER_ADDRESS]
+                state,
+                node.constraints + [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF],
             )
             description = "Anyone can kill this contract and withdraw its balance to their own account."
         except UnsatError:
-            transaction_sequence = solver.get_transaction_sequence(state, constraints)
+            transaction_sequence = solver.get_transaction_sequence(
+                state, node.constraints
+            )
             description = (
                 "The contract can be killed by anyone. Don't accidentally kill it."
             )

mythril/analysis/solver.py

@@ -103,7 +103,7 @@ def get_transaction_sequence(global_state, constraints):
         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.concretized(model)
+                for b in transaction.call_data.concrete(model)
             ]
         )
 

mythril/interfaces/cli.py

@@ -385,7 +385,6 @@ def main():
                     max_depth=args.max_depth,
                     execution_timeout=args.execution_timeout,
                     create_timeout=args.create_timeout,
-                    transaction_count=1,
                 )
 
                 try:

mythril/laser/ethereum/call.py

@@ -3,7 +3,11 @@ from typing import Union
 from z3 import simplify, ExprRef, Extract
 import mythril.laser.ethereum.util as util
 from mythril.laser.ethereum.state.account import Account
-from mythril.laser.ethereum.state.calldata import CalldataType, Calldata
+from mythril.laser.ethereum.state.calldata import (
+    CalldataType,
+    SymbolicCalldata,
+    ConcreteCalldata,
+)
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.support.loader import DynLoader
 import re
@@ -162,12 +166,12 @@ def get_call_data(
         ]
         i = 0
 
-        call_data = Calldata(transaction_id, calldata_from_mem)
+        call_data = ConcreteCalldata(transaction_id, calldata_from_mem)
         call_data_type = CalldataType.CONCRETE
         logging.debug("Calldata: " + str(call_data))
     except TypeError:
         logging.debug("Unsupported symbolic calldata offset")
         call_data_type = CalldataType.SYMBOLIC
-        call_data = Calldata("{}_internalcall".format(transaction_id))
+        call_data = SymbolicCalldata("{}_internalcall".format(transaction_id))
 
     return call_data, call_data_type

mythril/laser/ethereum/instructions.py

@@ -42,7 +42,7 @@ from mythril.laser.ethereum.evm_exceptions import (
 )
 from mythril.laser.ethereum.gas import OPCODE_GAS
 from mythril.laser.ethereum.keccak import KeccakFunctionManager
-from mythril.laser.ethereum.state.calldata import CalldataType, Calldata
+from mythril.laser.ethereum.state.calldata import CalldataType
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction import (
     MessageCallTransaction,
@@ -458,10 +458,9 @@ class Instruction:
         environment = global_state.environment
         op0 = state.stack.pop()
 
-        value, constraints = environment.calldata.get_word_at(op0)
+        value = environment.calldata.get_word_at(op0)
 
         state.stack.append(value)
-        state.constraints.extend(constraints)
 
         return [global_state]
 
@@ -541,9 +540,8 @@ class Instruction:
                 i_data = dstart
                 new_memory = []
                 for i in range(size):
-                    value, constraints = environment.calldata[i_data]
+                    value = environment.calldata[i_data]
                     new_memory.append(value)
-                    state.constraints.extend(constraints)
 
                     i_data = (
                         i_data + 1 if isinstance(i_data, int) else simplify(i_data + 1)
@@ -775,6 +773,14 @@ class Instruction:
 
         return [global_state]
 
+    @StateTransition()
+    def returndatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
+        # FIXME: not implemented
+        state = global_state.mstate
+        start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop()
+
+        return [global_state]
+
     @StateTransition()
     def returndatasize_(self, global_state: GlobalState) -> List[GlobalState]:
         global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256))

mythril/laser/ethereum/natives.py

@@ -8,7 +8,7 @@ from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n
 from rlp.utils import ALL_BYTES
 
-from mythril.laser.ethereum.state.calldata import Calldata
+from mythril.laser.ethereum.state.calldata import BaseCalldata
 from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int
 from z3 import Concat, simplify
 
@@ -88,7 +88,7 @@ def identity(data: Union[bytes, str, List[int]]) -> bytes:
     return result
 
 
-def native_contracts(address: int, data: Calldata):
+def native_contracts(address: int, data: BaseCalldata):
     """
     takes integer address 1, 2, 3, 4
     """

mythril/laser/ethereum/state/account.py

@@ -1,6 +1,6 @@
 from typing import Dict, Union, Any, KeysView
 
-from z3 import BitVec, ExprRef
+from z3 import BitVec, BitVecVal, ExprRef
 
 from mythril.disassembler.disassembly import Disassembly
 
@@ -41,7 +41,7 @@ class Storage:
                     pass
         if self.concrete:
             return 0
-        self._storage[item] = BitVec("storage_" + str(item), 256)
+        self._storage[item] = BitVecVal(0, 256)
         return self._storage[item]
 
     def __setitem__(self, key: str, value: ExprRef) -> None:

mythril/laser/ethereum/state/calldata.py

@@ -1,17 +1,7 @@
 from enum import Enum
 from typing import Union, Any
-from z3 import (
-    BitVecVal,
-    BitVecRef,
-    BitVecSort,
-    BitVec,
-    Implies,
-    simplify,
-    Concat,
-    UGT,
-    Array,
-)
-from z3.z3types import Z3Exception
+from z3 import BitVecVal, BitVecRef, BitVec, simplify, Concat, If, ExprRef
+from z3.z3types import Z3Exception, Model
 
 from mythril.laser.ethereum.util import get_concrete_int
 
@@ -21,84 +11,132 @@ class CalldataType(Enum):
     SYMBOLIC = 2
 
 
-class Calldata:
+class BaseCalldata:
     """
-    Calldata class representing the calldata of a transaction
+    Base calldata class
+    This represents the calldata provided when sending a transaction to a contract
     """
 
-    def __init__(self, tx_id, starting_calldata=None):
-        """
-        Constructor for Calldata
-        :param tx_id: unique value representing the transaction the calldata is for
-        :param starting_calldata: byte array representing the concrete calldata of a transaction
-        """
+    def __init__(self, tx_id):
         self.tx_id = tx_id
-        if starting_calldata is not None:
-            self._calldata = []
-            self.calldatasize = BitVecVal(len(starting_calldata), 256)
-            self.concrete = True
-        else:
-            self._calldata = Array(
-                "{}_calldata".format(self.tx_id), BitVecSort(256), BitVecSort(8)
-            )
-            self.calldatasize = BitVec("{}_calldatasize".format(self.tx_id), 256)
-            self.concrete = False
-
-        if self.concrete:
-            for calldata_byte in starting_calldata:
-                if type(calldata_byte) == int:
-                    self._calldata.append(BitVecVal(calldata_byte, 8))
-                else:
-                    self._calldata.append(calldata_byte)
-
-    def concretized(self, model):
-        result = []
-        for i in range(
-            get_concrete_int(model.eval(self.calldatasize, model_completion=True))
-        ):
-            result.append(
-                get_concrete_int(model.eval(self._calldata[i], model_completion=True))
-            )
 
+    @property
+    def calldatasize(self) -> ExprRef:
+        """
+        :return: Calldata size for this calldata object
+        """
+        result = self.size
+        if isinstance(result, int):
+            return BitVecVal(result, 256)
         return result
 
-    def get_word_at(self, index: int):
-        return self[index : index + 32]
+    def get_word_at(self, offset: int) -> ExprRef:
+        """ Gets word at offset"""
+        return self[offset : offset + 32]
 
     def __getitem__(self, item: Union[int, slice]) -> Any:
+        if isinstance(item, int) or isinstance(item, ExprRef):
+            return self._load(item)
+
         if isinstance(item, slice):
-            start, step, stop = item.start, item.step, item.stop
+            start = 0 if item.start is None else item.start
+            step = 1 if item.step is None else item.step
+            stop = self.size if item.stop is None else item.stop
+
             try:
-                if start is None:
-                    start = 0
-                if step is None:
-                    step = 1
-                if stop is None:
-                    stop = self.calldatasize
                 current_index = (
                     start if isinstance(start, BitVecRef) else BitVecVal(start, 256)
                 )
-                dataparts = []
+                parts = []
                 while simplify(current_index != stop):
-                    dataparts.append(self[current_index])
+                    parts.append(self._load(current_index))
                     current_index = simplify(current_index + step)
             except Z3Exception:
                 raise IndexError("Invalid Calldata Slice")
 
-            values, constraints = zip(*dataparts)
-            result_constraints = []
-            for c in constraints:
-                result_constraints.extend(c)
-            return simplify(Concat(values)), result_constraints
+            return simplify(Concat(parts))
+
+        raise ValueError
+
+    def _load(self, item: Union[int, ExprRef]) -> Any:
+        raise NotImplementedError()
+
+    @property
+    def size(self) -> Union[ExprRef, int]:
+        """ Returns the exact size of this calldata, this is not normalized"""
+        raise NotImplementedError()
+
+    def concrete(self, model: Model) -> list:
+        """ Returns a concrete version of the calldata using the provided model"""
+        raise NotImplementedError
+
+
+class ConcreteCalldata(BaseCalldata):
+    def __init__(self, tx_id: int, calldata: list):
+        """
+        Initializes the ConcreteCalldata object
+        :param tx_id: Id of the transaction that the calldata is for.
+        :param calldata: The concrete calldata content
+        """
+        self._calldata = calldata
+        super().__init__(tx_id)
 
-        if self.concrete:
+    def _load(self, item: Union[int, ExprRef]) -> Any:
+        if isinstance(item, int):
             try:
-                return self._calldata[get_concrete_int(item)], ()
+                return self._calldata[item]
             except IndexError:
-                return BitVecVal(0, 8), ()
-        else:
-            constraints = [
-                Implies(self._calldata[item] != 0, UGT(self.calldatasize, item))
-            ]
+                return 0
+
+        value = BitVecVal(0x0, 8)
+        for i in range(self.size):
+            value = If(item == i, self._calldata[i], value)
+        return value
+
+    def concrete(self, model: Model) -> list:
+        return self._calldata
+
+    @property
+    def size(self) -> int:
+        return len(self._calldata)
+
+
+class SymbolicCalldata(BaseCalldata):
+    def __init__(self, tx_id: int):
+        """
+        Initializes the SymbolicCalldata object
+        :param tx_id: Id of the transaction that the calldata is for.
+        """
+        self._reads = []
+        self._size = BitVec(str(tx_id) + "_calldatasize", 256)
+        super().__init__(tx_id)
+
+    def _load(self, item: Union[int, ExprRef], clean=False) -> Any:
+        x = BitVecVal(item, 256) if isinstance(item, int) else item
+
+        symbolic_base_value = If(
+            x >= self._size,
+            BitVecVal(0, 8),
+            BitVec("{}_calldata_{}".format(self.tx_id, str(item)), 8),
+        )
+        return_value = symbolic_base_value
+        for r_index, r_value in self._reads:
+            return_value = If(r_index == item, r_value, return_value)
+
+        if not clean:
+            self._reads.append((item, symbolic_base_value))
+        return simplify(return_value)
+
+    def concrete(self, model: Model) -> list:
+        concrete_length = get_concrete_int(model.eval(self.size, model_completion=True))
+        result = []
+        for i in range(concrete_length):
+            value = self._load(i, clean=True)
+            c_value = get_concrete_int(model.eval(value, model_completion=True))
+            result.append(c_value)
+
+        return result
 
-            return self._calldata[item], constraints
+    @property
+    def size(self) -> ExprRef:
+        return self._size

mythril/laser/ethereum/state/environment.py

@@ -3,7 +3,7 @@ from typing import Dict
 from z3 import ExprRef, BitVecVal
 
 from mythril.laser.ethereum.state.account import Account
-from mythril.laser.ethereum.state.calldata import Calldata, CalldataType
+from mythril.laser.ethereum.state.calldata import CalldataType, BaseCalldata
 
 
 class Environment:
@@ -15,7 +15,7 @@ class Environment:
         self,
         active_account: Account,
         sender: ExprRef,
-        calldata: Calldata,
+        calldata: BaseCalldata,
         gasprice: ExprRef,
         callvalue: ExprRef,
         origin: ExprRef,

mythril/laser/ethereum/transaction/concolic.py

@@ -6,7 +6,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 )
 from z3 import BitVec
 from mythril.laser.ethereum.state.environment import Environment
-from mythril.laser.ethereum.state.calldata import Calldata, CalldataType
+from mythril.laser.ethereum.state.calldata import CalldataType, ConcreteCalldata
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -42,7 +42,7 @@ def execute_message_call(
             code=Disassembly(code),
             caller=caller_address,
             callee_account=open_world_state[callee_address],
-            call_data=Calldata(next_transaction_id, data),
+            call_data=ConcreteCalldata(next_transaction_id, data),
             call_data_type=CalldataType.SYMBOLIC,
             call_value=value,
         )

mythril/laser/ethereum/transaction/symbolic.py

@@ -1,9 +1,13 @@
-from z3 import BitVec, Extract, Not
+from z3 import BitVec, BitVecVal
 from logging import debug
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
-from mythril.laser.ethereum.state.calldata import CalldataType, Calldata
+from mythril.laser.ethereum.state.calldata import (
+    CalldataType,
+    BaseCalldata,
+    SymbolicCalldata,
+)
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
@@ -12,6 +16,10 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 )
 
 
+CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
+ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
+
+
 def execute_message_call(laser_evm, callee_address: str) -> None:
     """ Executes a message call transaction from all open states """
     # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
@@ -30,9 +38,9 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
             gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
             gas_limit=8000000,  # block gas limit
             origin=BitVec("origin{}".format(next_transaction_id), 256),
-            caller=BitVec("caller{}".format(next_transaction_id), 256),
+            caller=BitVecVal(ATTACKER_ADDRESS, 256),
             callee_account=open_world_state[callee_address],
-            call_data=Calldata(next_transaction_id),
+            call_data=SymbolicCalldata(next_transaction_id),
             call_data_type=CalldataType.SYMBOLIC,
             call_value=BitVec("call_value{}".format(next_transaction_id), 256),
         )
@@ -64,7 +72,7 @@ def execute_contract_creation(
             gas_limit=8000000,  # block gas limit
             origin=BitVec("origin{}".format(next_transaction_id), 256),
             code=Disassembly(contract_initialization_code),
-            caller=BitVec("creator{}".format(next_transaction_id), 256),
+            caller=BitVecVal(CREATOR_ADDRESS, 256),
             callee_account=new_account,
             call_data=[],
             call_data_type=CalldataType.SYMBOLIC,

mythril/laser/ethereum/transaction/transaction_models.py

@@ -2,7 +2,11 @@ import logging
 from typing import Union
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.state.environment import Environment
-from mythril.laser.ethereum.state.calldata import Calldata
+from mythril.laser.ethereum.state.calldata import (
+    BaseCalldata,
+    ConcreteCalldata,
+    SymbolicCalldata,
+)
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -75,9 +79,9 @@ class BaseTransaction:
         self.caller = caller
         self.callee_account = callee_account
         if call_data is None and init_call_data:
-            self.call_data = Calldata(self.id, call_data)
+            self.call_data = ConcreteCalldata(self.id, call_data)
         else:
-            self.call_data = call_data if isinstance(call_data, Calldata) else None
+            self.call_data = call_data if isinstance(call_data, BaseCalldata) else None
         self.call_data_type = (
             call_data_type
             if call_data_type is not None

mythril/support/signatures.py

@@ -129,7 +129,7 @@ class SignatureDB(object):
         if (
             not self.enable_online_lookup
             or byte_sig in self.online_lookup_miss
-            or time.time() < self.online_lookup_timeout,
+            or time.time() < self.online_lookup_timeout
         ):
             return []
 

mythril/version.py

@@ -1,3 +1,3 @@
 # This file is suitable for sourcing inside POSIX shell, e.g. bash as
 # well as for importing into Python
-VERSION = "v0.19.7"  # NOQA
+VERSION = "v0.19.8"  # NOQA

tests/analysis/test_delegatecall.py

@@ -1,268 +0,0 @@
-from mythril.analysis.modules.delegatecall import detector
-from mythril.analysis.ops import Call, Variable, VarType
-from mythril.analysis.symbolic import SymExecWrapper
-from mythril.laser.ethereum.cfg import Node
-from mythril.laser.ethereum.state.environment import Environment
-from mythril.laser.ethereum.state.account import Account
-from mythril.laser.ethereum.state.global_state import GlobalState
-import pytest
-from unittest.mock import MagicMock, patch
-import pytest_mock
-from mythril.disassembler.disassembly import Disassembly
-
-
-def test_concrete_call():
-    # arrange
-    address = "0x10"
-    active_account = Account(address)
-    active_account.code = Disassembly("00")
-    environment = Environment(active_account, None, None, None, None, None)
-
-    state = GlobalState(None, environment, None)
-    state.mstate.memory = ["placeholder", "calldata_bling_0"]
-
-    node = Node("example")
-    node.contract_name = "the contract name"
-    node.function_name = "the function name"
-
-    to = Variable(1, VarType.CONCRETE)
-    meminstart = Variable(1, VarType.CONCRETE)
-    call = Call(node, state, None, None, to, None)
-
-    # act
-    issues = detector._concrete_call(call, state, address, meminstart)
-
-    # assert
-    issue = issues[0]
-    assert issue.address == address
-    assert issue.contract == node.contract_name
-    assert issue.function == node.function_name
-    assert issue.title == "Call data forwarded with delegatecall()"
-    assert issue.type == "Informational"
-    assert (
-        issue.description
-        == "This contract forwards its call data via DELEGATECALL in its fallback function."
-        " This means that any function in the called contract can be executed."
-        " Note that the callee contract will have access to the storage of the "
-        "calling contract.\nDELEGATECALL target: 0x1"
-    )
-
-
-def test_concrete_call_symbolic_to():
-    # arrange
-    address = "0x10"
-
-    active_account = Account(address)
-    active_account.code = Disassembly("00")
-    environment = Environment(active_account, None, None, None, None, None)
-    state = GlobalState(None, environment, None)
-    state.mstate.memory = ["placeholder", "calldata_bling_0"]
-
-    node = Node("example")
-    node.contract_name = "the contract name"
-    node.function_name = "the function name"
-
-    to = Variable("calldata_3", VarType.SYMBOLIC)
-    meminstart = Variable(1, VarType.CONCRETE)
-    call = Call(node, state, None, None, to, None)
-
-    # act
-    issues = detector._concrete_call(call, state, address, meminstart)
-
-    # assert
-    issue = issues[0]
-    assert issue.address == address
-    assert issue.contract == node.contract_name
-    assert issue.function == node.function_name
-    assert issue.title == "Call data forwarded with delegatecall()"
-    assert issue.type == "Informational"
-    assert issue.description == (
-        "This contract forwards its call data via DELEGATECALL in its fallback function."
-        " This means that any function in the called contract can be executed."
-        " Note that the callee contract will have access to the storage of the "
-        "calling contract.\nDELEGATECALL target: calldata_3"
-    )
-
-
-def test_concrete_call_not_calldata():
-    # arrange
-    state = GlobalState(None, None, None)
-    state.mstate.memory = ["placeholder", "not_calldata"]
-    meminstart = Variable(1, VarType.CONCRETE)
-
-    # act
-    issues = detector._concrete_call(None, state, None, meminstart)
-
-    # assert
-    assert issues == []
-
-
-def test_symbolic_call_storage_to(mocker):
-    # arrange
-    address = "0x10"
-
-    active_account = Account(address)
-    active_account.code = Disassembly("00")
-    environment = Environment(active_account, None, None, None, None, None)
-    state = GlobalState(None, environment, None)
-    state.mstate.memory = ["placeholder", "calldata_bling_0"]
-
-    node = Node("example")
-    node.contract_name = "the contract name"
-    node.function_name = "the function name"
-
-    to = Variable("storage_1", VarType.SYMBOLIC)
-    call = Call(node, state, None, "Type: ", to, None)
-
-    mocker.patch.object(SymExecWrapper, "__init__", lambda x, y: None)
-    statespace = SymExecWrapper(1)
-
-    mocker.patch.object(statespace, "find_storage_write")
-    statespace.find_storage_write.return_value = "Function name"
-
-    # act
-    issues = detector._symbolic_call(call, state, address, statespace)
-
-    # assert
-    issue = issues[0]
-    assert issue.address == address
-    assert issue.contract == node.contract_name
-    assert issue.function == node.function_name
-    assert issue.title == "Type:  to a user-supplied address"
-    assert issue.type == "Informational"
-    assert issue.description == (
-        "This contract delegates execution to a contract address in storage slot 1."
-        " This storage slot can be written to by calling the function `Function name`."
-        " Be aware that the called contract gets unrestricted access to this contract's state."
-    )
-
-
-def test_symbolic_call_calldata_to(mocker):
-    # arrange
-    address = "0x10"
-
-    active_account = Account(address)
-    active_account.code = Disassembly("00")
-    environment = Environment(active_account, None, None, None, None, None)
-    state = GlobalState(None, environment, None)
-    state.mstate.memory = ["placeholder", "calldata_bling_0"]
-
-    node = Node("example")
-    node.contract_name = "the contract name"
-    node.function_name = "the function name"
-
-    to = Variable("calldata", VarType.SYMBOLIC)
-    call = Call(node, state, None, "Type: ", to, None)
-
-    mocker.patch.object(SymExecWrapper, "__init__", lambda x, y: None)
-    statespace = SymExecWrapper(1)
-
-    mocker.patch.object(statespace, "find_storage_write")
-    statespace.find_storage_write.return_value = "Function name"
-
-    # act
-    issues = detector._symbolic_call(call, state, address, statespace)
-
-    # assert
-    issue = issues[0]
-    assert issue.address == address
-    assert issue.contract == node.contract_name
-    assert issue.function == node.function_name
-    assert issue.title == "Type:  to a user-supplied address"
-    assert issue.type == "Informational"
-    assert issue.description == (
-        "This contract delegates execution to a contract address obtained from calldata."
-        " Be aware that the called contract gets unrestricted access to this contract's state."
-    )
-
-
-@patch("mythril.laser.ethereum.state.global_state.GlobalState.get_current_instruction")
-@patch("mythril.analysis.modules.delegatecall.detector._concrete_call")
-@patch("mythril.analysis.modules.delegatecall.detector._symbolic_call")
-def test_delegate_call(sym_mock, concrete_mock, curr_instruction):
-    # arrange
-    # sym_mock = mocker.patch.object(delegatecall, "_symbolic_call")
-    # concrete_mock = mocker.patch.object(delegatecall, "_concrete_call")
-    sym_mock.return_value = []
-    concrete_mock.return_value = []
-    curr_instruction.return_value = {"address": "0x10"}
-
-    active_account = Account("0x10")
-    active_account.code = Disassembly("00")
-
-    environment = Environment(active_account, None, None, None, None, None)
-    state = GlobalState(None, environment, Node)
-    state.mstate.memory = ["placeholder", "calldata_bling_0"]
-    state.mstate.stack = [1, 2, 3]
-    assert state.get_current_instruction() == {"address": "0x10"}
-
-    node = Node("example")
-    node.contract_name = "the contract name"
-    node.function_name = "fallback"
-
-    to = Variable("storage_1", VarType.SYMBOLIC)
-    call = Call(node, state, None, "DELEGATECALL", to, None)
-
-    statespace = MagicMock()
-    statespace.calls = [call]
-
-    # act
-    detector.execute(statespace)
-
-    # assert
-    assert concrete_mock.call_count == 1
-    assert sym_mock.call_count == 1
-
-
-@patch("mythril.analysis.modules.delegatecall.detector._concrete_call")
-@patch("mythril.analysis.modules.delegatecall.detector._symbolic_call")
-def test_delegate_call_not_delegate(sym_mock, concrete_mock):
-    # arrange
-    # sym_mock = mocker.patch.object(delegatecall, "_symbolic_call")
-    # concrete_mock = mocker.patch.object(delegatecall, "_concrete_call")
-    sym_mock.return_value = []
-    concrete_mock.return_value = []
-
-    node = Node("example")
-    node.function_name = "fallback"
-
-    to = Variable("storage_1", VarType.SYMBOLIC)
-    call = Call(node, None, None, "NOT_DELEGATECALL", to, None)
-
-    statespace = MagicMock()
-    statespace.calls = [call]
-
-    # act
-    issues = detector.execute(statespace)
-
-    # assert
-    assert issues == []
-    assert concrete_mock.call_count == 0
-    assert sym_mock.call_count == 0
-
-
-@patch("mythril.analysis.modules.delegatecall.detector._concrete_call")
-@patch("mythril.analysis.modules.delegatecall.detector._symbolic_call")
-def test_delegate_call_not_fallback(sym_mock, concrete_mock):
-    # arrange
-    # sym_mock = mocker.patch.object(delegatecall, "_symbolic_call")
-    # concrete_mock = mocker.patch.object(delegatecall, "_concrete_call")
-    sym_mock.return_value = []
-    concrete_mock.return_value = []
-
-    node = Node("example")
-    node.function_name = "not_fallback"
-
-    to = Variable("storage_1", VarType.SYMBOLIC)
-    call = Call(node, None, None, "DELEGATECALL", to, None)
-
-    statespace = MagicMock()
-    statespace.calls = [call]
-
-    # act
-    issues = detector.execute(statespace)
-
-    # assert
-    assert issues == []
-    assert concrete_mock.call_count == 0
-    assert sym_mock.call_count == 0

tests/cmd_line_test.py

@@ -26,7 +26,7 @@ class CommandLineToolTestCase(BaseTestCase):
 class TruffleTestCase(BaseTestCase):
     def test_analysis_truffle_project(self):
         truffle_project_root = str(TESTS_DIR / "truffle_project")
-        command = "cd {}; truffle compile; python3 {} --truffle -t 1".format(
+        command = "cd {}; truffle compile; python3 {} --truffle -t 2".format(
             truffle_project_root, MYTH
         )
         self.assertIn("=== Ether thief ====", output_of(command))

tests/laser/state/calldata_test.py

@@ -1,6 +1,6 @@
 import pytest
-from mythril.laser.ethereum.state.calldata import Calldata
-from z3 import Solver, simplify
+from mythril.laser.ethereum.state.calldata import ConcreteCalldata, SymbolicCalldata
+from z3 import Solver, simplify, BitVec, sat, unsat
 from z3.z3types import Z3Exception
 from mock import MagicMock
 
@@ -13,21 +13,11 @@ uninitialized_test_data = [
 @pytest.mark.parametrize("starting_calldata", uninitialized_test_data)
 def test_concrete_calldata_uninitialized_index(starting_calldata):
     # Arrange
-    calldata = Calldata(0, starting_calldata)
-    solver = Solver()
+    calldata = ConcreteCalldata(0, starting_calldata)
 
     # Act
-    value, constraint1 = calldata[100]
-    value2, constraint2 = calldata.get_word_at(200)
-
-    solver.add(constraint1)
-    solver.add(constraint2)
-
-    solver.check()
-    model = solver.model()
-
-    value = model.eval(value)
-    value2 = model.eval(value2)
+    value = calldata[100]
+    value2 = calldata.get_word_at(200)
 
     # Assert
     assert value == 0
@@ -36,73 +26,65 @@ def test_concrete_calldata_uninitialized_index(starting_calldata):
 
 def test_concrete_calldata_calldatasize():
     # Arrange
-    calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9])
+    calldata = ConcreteCalldata(0, [1, 4, 7, 3, 7, 2, 9])
     solver = Solver()
 
     # Act
     solver.check()
     model = solver.model()
-
     result = model.eval(calldata.calldatasize)
 
     # Assert
     assert result == 7
 
 
-def test_symbolic_calldata_constrain_index():
+def test_concrete_calldata_constrain_index():
     # Arrange
-    calldata = Calldata(0)
+    calldata = ConcreteCalldata(0, [1, 4, 7, 3, 7, 2, 9])
     solver = Solver()
 
     # Act
-    value, calldata_constraints = calldata[100]
-    constraint = value == 50
-
-    solver.add([constraint] + calldata_constraints)
-
-    solver.check()
-    model = solver.model()
+    value = calldata[2]
+    constraint = value == 3
 
-    value = model.eval(value)
-    calldatasize = model.eval(calldata.calldatasize)
+    solver.add([constraint])
+    result = solver.check()
 
     # Assert
-    assert value == 50
-    assert simplify(calldatasize >= 100)
+    assert str(result) == "unsat"
 
 
-def test_concrete_calldata_constrain_index():
+def test_symbolic_calldata_constrain_index():
     # Arrange
-    calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9])
+    calldata = SymbolicCalldata(0)
     solver = Solver()
 
     # Act
-    value, calldata_constraints = calldata[2]
-    constraint = value == 3
+    value = calldata[51]
+
+    constraints = [value == 1, calldata.calldatasize == 50]
+
+    solver.add(constraints)
 
-    solver.add([constraint] + calldata_constraints)
     result = solver.check()
 
     # Assert
     assert str(result) == "unsat"
 
 
-def test_concrete_calldata_constrain_index():
-    # Arrange
-    calldata = Calldata(0)
-    mstate = MagicMock()
-    mstate.constraints = []
-    solver = Solver()
+def test_symbolic_calldata_equal_indices():
+    calldata = SymbolicCalldata(0)
 
-    # Act
-    constraints = []
-    value, calldata_constraints = calldata[51]
-    constraints.append(value == 1)
-    constraints.append(calldata.calldatasize == 50)
+    index_a = BitVec("index_a", 256)
+    index_b = BitVec("index_b", 256)
 
-    solver.add(constraints + calldata_constraints)
+    # Act
+    a = calldata[index_a]
+    b = calldata[index_b]
 
-    result = solver.check()
+    s = Solver()
+    s.append(index_a == index_b)
+    s.append(a != b)
 
     # Assert
-    assert str(result) == "unsat"
+    assert unsat == s.check()

tests/testdata/input_contracts/calls.sol

@@ -9,7 +9,7 @@ contract Caller {
 	uint256 statevar;
 
 	constructor(address addr) public {
-		fixed_address = addr;
+		fixed_address = address(0x552254CbAaF32613C6c0450CF19524594eF84044);
 	}
 
 	function thisisfine() public {
@@ -27,6 +27,7 @@ contract Caller {
 
 	function callstoredaddress() public {
 	    stored_address.call("");
+	    statevar = 0;
 	}
 
 	function setstoredaddress(address addr) public {

tests/testdata/input_contracts/overflow.sol

@@ -11,7 +11,7 @@ contract Over {
   }
 
   function sendeth(address _to, uint _value) public returns (bool) {
-    require(balances[msg.sender] - _value >= 0);
+    // require(balances[msg.sender] - _value >= 0);
     balances[msg.sender] -= _value;
     balances[_to] += _value;
     return true;

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

@@ -1,126 +1 @@
-{
-  "error": null,
-  "issues": [
-    {
-      "address": 661,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
-      "function": "thisisfine()",
-      "swc-id": "107",
-      "min_gas_used": 643,
-      "max_gas_used": 1254,
-      "title": "Message call to external contract",
-      "type": "Informational"
-    },
-    {
-      "address": 666,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "thisisfine()",
-      "swc-id": "104",
-      "min_gas_used": 1352,
-      "max_gas_used": 35963,
-      "title": "Unchecked CALL return value",
-      "type": "Informational"
-    },
-    {
-      "address": 779,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This contract executes a message call to an address found at storage slot 1. This storage slot can be written to by calling the function `setstoredaddress(address)`. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.",
-      "function": "callstoredaddress()",
-      "swc-id": "107",
-      "min_gas_used": 687,
-      "max_gas_used": 1298,
-      "title": "Message call to external contract",
-      "type": "Warning"
-    },
-    {
-      "address": 779,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "Possible transaction order dependence vulnerability: The value or direction of the call statement is determined from a tainted storage location.",
-      "function": "callstoredaddress()",
-      "swc-id": "114",
-      "min_gas_used": 687,
-      "max_gas_used": 1298,
-      "title": "Transaction order dependence",
-      "type": "Warning"
-    },
-    {
-      "address": 784,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "callstoredaddress()",
-      "swc-id": "104",
-      "min_gas_used": 1396,
-      "max_gas_used": 36007,
-      "title": "Unchecked CALL return value",
-      "type": "Informational"
-    },
-    {
-      "address": 858,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
-      "function": "reentrancy()",
-      "swc-id": "107",
-      "min_gas_used": 709,
-      "max_gas_used": 1320,
-      "title": "Message call to external contract",
-      "type": "Informational"
-    },
-    {
-      "address": 869,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The contract account state is changed after an external call. Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.",
-      "function": "reentrancy()",
-      "swc-id": "107",
-      "min_gas_used": 709,
-      "max_gas_used": 1320,
-      "title": "State change after external call",
-      "type": "Warning"
-    },
-    {
-      "address": 871,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "reentrancy()",
-      "swc-id": "104",
-      "min_gas_used": 6432,
-      "max_gas_used": 61043,
-      "title": "Unchecked CALL return value",
-      "type": "Informational"
-    },
-    {
-      "address": 912,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.",
-      "function": "calluseraddress(address)",
-      "swc-id": "107",
-      "min_gas_used": 335,
-      "max_gas_used": 616,
-      "title": "Message call to external contract",
-      "type": "Warning"
-    },
-    {
-      "address": 918,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "calluseraddress(address)",
-      "swc-id": "104",
-      "min_gas_used": 1046,
-      "max_gas_used": 35327,
-      "title": "Unchecked CALL return value",
-      "type": "Informational"
-    }
-  ],
-  "success": true
-}
+{"error": null, "issues": [{"address": 661, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.", "function": "thisisfine()", "max_gas_used": 1254, "min_gas_used": 643, "swc-id": "107", "title": "External call", "type": "Informational"}, {"address": 666, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "thisisfine()", "max_gas_used": 35963, "min_gas_used": 1352, "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 779, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.", "function": "callstoredaddress()", "max_gas_used": 1298, "min_gas_used": 687, "swc-id": "107", "title": "External call", "type": "Informational"}, {"address": 784, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "callstoredaddress()", "max_gas_used": 36007, "min_gas_used": 1396, "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 858, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.", "function": "reentrancy()", "max_gas_used": 1320, "min_gas_used": 709, "swc-id": "107", "title": "External call", "type": "Informational"}, {"address": 871, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "reentrancy()", "max_gas_used": 61043, "min_gas_used": 6432, "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 912, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes a function call with high gas to a user-supplied address. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent unanticipated effects on the contract state.", "function": "calluseraddress(address)", "max_gas_used": 616, "min_gas_used": 335, "swc-id": "107", "title": "External call to user-supplied address", "type": "Warning"}, {"address": 918, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "calluseraddress(address)", "max_gas_used": 35327, "min_gas_used": 1046, "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}], "success": true}

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

@@ -1,6 +1,6 @@
 # Analysis results for test-filename.sol
 
-## Message call to external contract
+## External call
 - SWC ID: 107
 - Type: Informational
 - Contract: Unknown
@@ -10,7 +10,7 @@
 
 ### Description
 
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 
 ## Unchecked CALL return value
 - SWC ID: 104
@@ -24,21 +24,9 @@ This contract executes a message call to to another contract. Make sure that the
 
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 
-## Message call to external contract
+## External call
 - SWC ID: 107
-- Type: Warning
-- Contract: Unknown
-- Function name: `callstoredaddress()`
-- PC address: 779
-- Estimated Gas Usage: 687 - 1298
-
-### Description
-
-This contract executes a message call to an address found at storage slot 1. This storage slot can be written to by calling the function `setstoredaddress(address)`. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
-
-## Transaction order dependence
-- SWC ID: 114
-- Type: Warning
+- Type: Informational
 - Contract: Unknown
 - Function name: `callstoredaddress()`
 - PC address: 779
@@ -46,7 +34,7 @@ This contract executes a message call to an address found at storage slot 1. Thi
 
 ### Description
 
-Possible transaction order dependence vulnerability: The value or direction of the call statement is determined from a tainted storage location.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 
 ## Unchecked CALL return value
 - SWC ID: 104
@@ -60,7 +48,7 @@ Possible transaction order dependence vulnerability: The value or direction of t
 
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 
-## Message call to external contract
+## External call
 - SWC ID: 107
 - Type: Informational
 - Contract: Unknown
@@ -70,19 +58,7 @@ The return value of an external call is not checked. Note that execution continu
 
 ### Description
 
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
-
-## State change after external call
-- SWC ID: 107
-- Type: Warning
-- Contract: Unknown
-- Function name: `reentrancy()`
-- PC address: 869
-- Estimated Gas Usage: 709 - 1320
-
-### Description
-
-The contract account state is changed after an external call. Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 
 ## Unchecked CALL return value
 - SWC ID: 104
@@ -96,7 +72,7 @@ The contract account state is changed after an external call. Consider that the
 
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 
-## Message call to external contract
+## External call to user-supplied address
 - SWC ID: 107
 - Type: Warning
 - Contract: Unknown
@@ -106,7 +82,7 @@ The return value of an external call is not checked. Note that execution continu
 
 ### Description
 
-This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
+The contract executes a function call with high gas to a user-supplied address. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent unanticipated effects on the contract state.
 
 ## Unchecked CALL return value
 - SWC ID: 104

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

@@ -1,11 +1,11 @@
-==== Message call to external contract ====
+==== External call ====
 SWC ID: 107
 Type: Informational
 Contract: Unknown
 Function name: thisisfine()
 PC address: 661
 Estimated Gas Usage: 643 - 1254
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 --------------------
 
 ==== Unchecked CALL return value ====
@@ -18,24 +18,14 @@ Estimated Gas Usage: 1352 - 35963
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
-==== Message call to external contract ====
+==== External call ====
 SWC ID: 107
-Type: Warning
-Contract: Unknown
-Function name: callstoredaddress()
-PC address: 779
-Estimated Gas Usage: 687 - 1298
-This contract executes a message call to an address found at storage slot 1. This storage slot can be written to by calling the function `setstoredaddress(address)`. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
---------------------
-
-==== Transaction order dependence ====
-SWC ID: 114
-Type: Warning
+Type: Informational
 Contract: Unknown
 Function name: callstoredaddress()
 PC address: 779
 Estimated Gas Usage: 687 - 1298
-Possible transaction order dependence vulnerability: The value or direction of the call statement is determined from a tainted storage location.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 --------------------
 
 ==== Unchecked CALL return value ====
@@ -48,24 +38,14 @@ Estimated Gas Usage: 1396 - 36007
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
-==== Message call to external contract ====
+==== External call ====
 SWC ID: 107
 Type: Informational
 Contract: Unknown
 Function name: reentrancy()
 PC address: 858
 Estimated Gas Usage: 709 - 1320
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
---------------------
-
-==== State change after external call ====
-SWC ID: 107
-Type: Warning
-Contract: Unknown
-Function name: reentrancy()
-PC address: 869
-Estimated Gas Usage: 709 - 1320
-The contract account state is changed after an external call. Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 --------------------
 
 ==== Unchecked CALL return value ====
@@ -78,14 +58,14 @@ Estimated Gas Usage: 6432 - 61043
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
-==== Message call to external contract ====
+==== External call to user-supplied address ====
 SWC ID: 107
 Type: Warning
 Contract: Unknown
 Function name: calluseraddress(address)
 PC address: 912
 Estimated Gas Usage: 335 - 616
-This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
+The contract executes a function call with high gas to a user-supplied address. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent unanticipated effects on the contract state.
 --------------------
 
 ==== Unchecked CALL return value ====

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

@@ -1,36 +1,36 @@
 {
-  "error": null,
-  "issues": [
-    {
-      "address": 158,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The arithmetic operation can result in integer overflow.\n",
-      "function": "_function_0x83f12fec",
-      "swc-id": "101",
-      "title": "Integer Overflow",
-      "type": "Warning"
-    },
-    {
-      "address": 278,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The arithmetic operation can result in integer overflow.\n",
-      "function": "_function_0x83f12fec",
-      "swc-id": "101",
-      "title": "Integer Overflow",
-      "type": "Warning"
-    },
-    {
-      "address": 378,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The substraction can result in an integer underflow.\n",
-      "function": "_function_0x83f12fec",
-      "swc-id": "101",
-      "title": "Integer Underflow",
-      "type": "Warning"
-    }
-  ],
-  "success": true
+    "error": null,
+    "issues": [
+        {
+            "address": 158,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The arithmetic operation can result in integer overflow.\n",
+            "function": "_function_0x83f12fec",
+            "swc-id": "101",
+            "title": "Integer Overflow",
+            "type": "Warning",
+        },
+        {
+            "address": 278,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The arithmetic operation can result in integer overflow.\n",
+            "function": "_function_0x83f12fec",
+            "swc-id": "101",
+            "title": "Integer Overflow",
+            "type": "Warning",
+        },
+        {
+            "address": 378,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The substraction can result in an integer underflow.\n",
+            "function": "_function_0x83f12fec",
+            "swc-id": "101",
+            "title": "Integer Underflow",
+            "type": "Warning",
+        },
+    ],
+    "success": true,
 }

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

@@ -1,30 +1,5 @@
 {
   "error": null,
-  "issues": [
-    {
-      "address": 722,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "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.",
-      "function": "withdrawfunds()",
-      "max_gas_used": 1749,
-      "min_gas_used": 1138,
-      "swc-id": "105",
-      "title": "Ether thief",
-      "type": "Warning"
-    },
-    {
-      "address": 883,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This binary add operation can result in integer overflow.\n",
-      "function": "invest()",
-      "max_gas_used": 1856,
-      "min_gas_used": 1571,
-      "swc-id": "101",
-      "title": "Integer Overflow",
-      "type": "Warning"
-    }
-  ],
+  "issues": [],
   "success": true
 }

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

@@ -1,25 +1,3 @@
-# Analysis results for test-filename.sol
+# Analysis results for None
 
-## Ether thief
-- SWC ID: 105
-- Type: Warning
-- Contract: Unknown
-- Function name: `withdrawfunds()`
-- PC address: 722
-- Estimated Gas Usage: 1138 - 1749
-
-### Description
-
-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.
-
-## Integer Overflow
-- SWC ID: 101
-- Type: Warning
-- Contract: Unknown
-- Function name: `invest()`
-- PC address: 883
-- Estimated Gas Usage: 1571 - 1856
-
-### Description
-
-This binary add operation can result in integer overflow.
+The analysis was completed successfully. No issues were detected.

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

@@ -1,21 +1 @@
-==== Ether thief ====
-SWC ID: 105
-Type: Warning
-Contract: Unknown
-Function name: withdrawfunds()
-PC address: 722
-Estimated Gas Usage: 1138 - 1749
-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.
---------------------
-
-==== Integer Overflow ====
-SWC ID: 101
-Type: Warning
-Contract: Unknown
-Function name: invest()
-PC address: 883
-Estimated Gas Usage: 1571 - 1856
-This binary add operation can result in integer overflow.
-
---------------------
-
+The analysis was completed successfully. No issues were detected.

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

@@ -7,9 +7,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "A reachable exception (opcode 0xfe) has been detected. This 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)",
-      "swc-id": "110",
-      "min_gas_used": 206,
       "max_gas_used": 301,
+      "min_gas_used": 206,
+      "swc-id": "110",
       "title": "Exception state",
       "type": "Informational"
     },
@@ -19,9 +19,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "A reachable exception (opcode 0xfe) has been detected. This 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)",
-      "swc-id": "110",
-      "min_gas_used": 256,
       "max_gas_used": 351,
+      "min_gas_used": 256,
+      "swc-id": "110",
       "title": "Exception state",
       "type": "Informational"
     },
@@ -31,9 +31,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "A reachable exception (opcode 0xfe) has been detected. This 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)",
-      "swc-id": "110",
-      "min_gas_used": 272,
       "max_gas_used": 367,
+      "min_gas_used": 272,
+      "swc-id": "110",
       "title": "Exception state",
       "type": "Informational"
     },
@@ -43,9 +43,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "A reachable exception (opcode 0xfe) has been detected. This 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()",
-      "swc-id": "110",
-      "min_gas_used": 268,
       "max_gas_used": 363,
+      "min_gas_used": 268,
+      "swc-id": "110",
       "title": "Exception state",
       "type": "Informational"
     }

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

@@ -29,12 +29,12 @@
             "address": 1038,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
-            "description": "This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.",
+            "description": "The contract executes a function call with high gas to a user-supplied address. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent unanticipated effects on the contract state.",
             "function": "_function_0xeea4c864",
             "max_gas_used": 1223,
             "min_gas_used": 471,
             "swc-id": "107",
-            "title": "Message call to external contract",
+            "title": "External call to user-supplied address",
             "type": "Warning"
         },
         {

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

@@ -24,7 +24,7 @@ The return value of an external call is not checked. Note that execution continu
 
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 
-## Message call to external contract
+## External call to user-supplied address
 - SWC ID: 107
 - Type: Warning
 - Contract: Unknown
@@ -34,7 +34,7 @@ The return value of an external call is not checked. Note that execution continu
 
 ### Description
 
-This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
+The contract executes a function call with high gas to a user-supplied address. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent unanticipated effects on the contract state.
 
 ## Unchecked CALL return value
 - SWC ID: 104

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

@@ -18,14 +18,14 @@ Estimated Gas Usage: 1161 - 35913
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
-==== Message call to external contract ====
+==== External call to user-supplied address ====
 SWC ID: 107
 Type: Warning
 Contract: Unknown
 Function name: _function_0xeea4c864
 PC address: 1038
 Estimated Gas Usage: 471 - 1223
-This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
+The contract executes a function call with high gas to a user-supplied address. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent unanticipated effects on the contract state.
 --------------------
 
 ==== Unchecked CALL return value ====

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

@@ -7,9 +7,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "The function `transferOwnership(address)` retrieves the transaction origin (tx.origin) using the ORIGIN opcode. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin",
       "function": "transferOwnership(address)",
-      "swc-id": "115",
-      "min_gas_used": 626,
       "max_gas_used": 1051,
+      "min_gas_used": 626,
+      "swc-id": "115",
       "title": "Use of tx.origin",
       "type": "Warning"
     }

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

@@ -7,9 +7,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "The subtraction can result in an integer underflow.\n",
       "function": "sendeth(address,uint256)",
-      "swc-id": "101",
-      "min_gas_used": 750,
       "max_gas_used": 1035,
+      "min_gas_used": 750,
+      "swc-id": "101",
       "title": "Integer Underflow",
       "type": "Warning"
     },
@@ -19,22 +19,10 @@
       "debug": "<DEBUG-DATA>",
       "description": "The subtraction can result in an integer underflow.\n",
       "function": "sendeth(address,uint256)",
-      "swc-id": "101",
-      "min_gas_used": 1283,
       "max_gas_used": 1758,
-      "title": "Integer Underflow",
-      "type": "Warning"
-    },
-    {
-      "address": 725,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This binary add operation can result in integer overflow.\n",
-      "function": "sendeth(address,uint256)",
+      "min_gas_used": 1283,
       "swc-id": "101",
-      "min_gas_used": 6806,
-      "max_gas_used": 27471,
-      "title": "Integer Overflow",
+      "title": "Integer Underflow",
       "type": "Warning"
     }
   ],

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

@@ -23,15 +23,3 @@ The subtraction can result in an integer underflow.
 ### Description
 
 The subtraction can result in an integer underflow.
-
-## Integer Overflow
-- SWC ID: 101
-- Type: Warning
-- Contract: Unknown
-- Function name: `sendeth(address,uint256)`
-- PC address: 725
-- Estimated Gas Usage: 6806 - 27471
-
-### Description
-
-This binary add operation can result in integer overflow.

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

@@ -20,14 +20,3 @@ The subtraction can result in an integer underflow.
 
 --------------------
 
-==== Integer Overflow ====
-SWC ID: 101
-Type: Warning
-Contract: Unknown
-Function name: sendeth(address,uint256)
-PC address: 725
-Estimated Gas Usage: 6806 - 27471
-This binary add operation can result in integer overflow.
-
---------------------
-

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

@@ -1,42 +1 @@
-{
-  "error": null,
-  "issues": [
-    {
-      "address": 196,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
-      "function": "callchecked()",
-      "swc-id": "107",
-      "min_gas_used": 599,
-      "max_gas_used": 1210,
-      "title": "Message call to external contract",
-      "type": "Informational"
-    },
-    {
-      "address": 285,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
-      "function": "callnotchecked()",
-      "swc-id": "107",
-      "min_gas_used": 621,
-      "max_gas_used": 1232,
-      "title": "Message call to external contract",
-      "type": "Informational"
-    },
-    {
-      "address": 290,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "callnotchecked()",
-      "swc-id": "104",
-      "min_gas_used": 1330,
-      "max_gas_used": 35941,
-      "title": "Unchecked CALL return value",
-      "type": "Informational"
-    }
-  ],
-  "success": true
-}
+{"error": null, "issues": [{"address": 196, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.", "function": "callchecked()", "max_gas_used": 1210, "min_gas_used": 599, "swc-id": "107", "title": "External call", "type": "Informational"}, {"address": 285, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.", "function": "callnotchecked()", "max_gas_used": 1232, "min_gas_used": 621, "swc-id": "107", "title": "External call", "type": "Informational"}, {"address": 290, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "callnotchecked()", "max_gas_used": 35941, "min_gas_used": 1330, "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}], "success": true}

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

@@ -1,6 +1,6 @@
 # Analysis results for test-filename.sol
 
-## Message call to external contract
+## External call
 - SWC ID: 107
 - Type: Informational
 - Contract: Unknown
@@ -10,9 +10,9 @@
 
 ### Description
 
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 
-## Message call to external contract
+## External call
 - SWC ID: 107
 - Type: Informational
 - Contract: Unknown
@@ -22,7 +22,7 @@ This contract executes a message call to to another contract. Make sure that the
 
 ### Description
 
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 
 ## Unchecked CALL return value
 - SWC ID: 104

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

@@ -1,21 +1,21 @@
-==== Message call to external contract ====
+==== External call ====
 SWC ID: 107
 Type: Informational
 Contract: Unknown
 Function name: callchecked()
 PC address: 196
 Estimated Gas Usage: 599 - 1210
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 --------------------
 
-==== Message call to external contract ====
+==== External call ====
 SWC ID: 107
 Type: Informational
 Contract: Unknown
 Function name: callnotchecked()
 PC address: 285
 Estimated Gas Usage: 621 - 1232
-This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
+The contract executes a function call to an external address. Verify that the code at this address is trusted and immutable.
 --------------------
 
 ==== Unchecked CALL return value ====

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

@@ -1,166 +1,166 @@
 {
-  "success": true,
-  "error": null,
-  "issues": [
-    {
-      "title": "Ether send",
-      "description": "In the function `_function_0x4229616d` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-      "function": "_function_0x4229616d",
-      "type": "Warning",
-      "address": 1599,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Ether send",
-      "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-      "function": "_function_0xb4022950",
-      "type": "Warning",
-      "address": 1940,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Ether send",
-      "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-      "function": "_function_0xb4022950",
-      "type": "Warning",
-      "address": 2582,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Exception state",
-      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-      "function": "_function_0x57d4021b",
-      "type": "Informational",
-      "address": 1653,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Exception state",
-      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-      "function": "_function_0x9dbc4f9b",
-      "type": "Informational",
-      "address": 2085,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "fallback",
-      "type": "Informational",
-      "address": 3111,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "fallback",
-      "type": "Informational",
-      "address": 3140,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "fallback",
-      "type": "Informational",
-      "address": 2950,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "fallback",
-      "type": "Informational",
-      "address": 1268,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x09dfdc71",
-      "type": "Informational",
-      "address": 310,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x09dfdc71",
-      "type": "Informational",
-      "address": 1316,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x253459e3",
-      "type": "Informational",
-      "address": 1375,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x4229616d",
-      "type": "Informational",
-      "address": 1511,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x57d4021b",
-      "type": "Informational",
-      "address": 1679,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x6fbaaa1e",
-      "type": "Informational",
-      "address": 618,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x8a5fb3ca",
-      "type": "Informational",
-      "address": 805,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Invariant branch condition",
-      "description": "Found a conditional jump which always follows the same branch",
-      "function": "_function_0x9dbc4f9b",
-      "type": "Informational",
-      "address": 2187,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Unchecked CALL return value",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "_function_0x4229616d",
-      "type": "Informational",
-      "address": 1599,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Unchecked CALL return value",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "_function_0xb4022950",
-      "type": "Informational",
-      "address": 1940,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Unchecked CALL return value",
-      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-      "function": "_function_0xb4022950",
-      "type": "Informational",
-      "address": 2582,
-      "debug": "<DEBUG-DATA>"
-    }
-  ]
+    "success": true,
+    "error": null,
+    "issues": [
+        {
+            "title": "Ether send",
+            "description": "In the function `_function_0x4229616d` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+            "function": "_function_0x4229616d",
+            "type": "Warning",
+            "address": 1599,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Ether send",
+            "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+            "function": "_function_0xb4022950",
+            "type": "Warning",
+            "address": 1940,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Ether send",
+            "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+            "function": "_function_0xb4022950",
+            "type": "Warning",
+            "address": 2582,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Exception state",
+            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+            "function": "_function_0x57d4021b",
+            "type": "Informational",
+            "address": 1653,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Exception state",
+            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+            "function": "_function_0x9dbc4f9b",
+            "type": "Informational",
+            "address": 2085,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "fallback",
+            "type": "Informational",
+            "address": 3111,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "fallback",
+            "type": "Informational",
+            "address": 3140,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "fallback",
+            "type": "Informational",
+            "address": 2950,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "fallback",
+            "type": "Informational",
+            "address": 1268,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x09dfdc71",
+            "type": "Informational",
+            "address": 310,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x09dfdc71",
+            "type": "Informational",
+            "address": 1316,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x253459e3",
+            "type": "Informational",
+            "address": 1375,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x4229616d",
+            "type": "Informational",
+            "address": 1511,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x57d4021b",
+            "type": "Informational",
+            "address": 1679,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x6fbaaa1e",
+            "type": "Informational",
+            "address": 618,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x8a5fb3ca",
+            "type": "Informational",
+            "address": 805,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Invariant branch condition",
+            "description": "Found a conditional jump which always follows the same branch",
+            "function": "_function_0x9dbc4f9b",
+            "type": "Informational",
+            "address": 2187,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Unchecked CALL return value",
+            "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+            "function": "_function_0x4229616d",
+            "type": "Informational",
+            "address": 1599,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Unchecked CALL return value",
+            "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+            "function": "_function_0xb4022950",
+            "type": "Informational",
+            "address": 1940,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Unchecked CALL return value",
+            "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+            "function": "_function_0xb4022950",
+            "type": "Informational",
+            "address": 2582,
+            "debug": "<DEBUG-DATA>",
+        },
+    ],
 }

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

@@ -1 +1,18 @@
-{"error": null, "issues": [{"address": 146, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "Anyone can kill this contract and withdraw its balance to their own account.", "function": "kill(address)", "max_gas_used": 263, "min_gas_used": 168, "swc-id": "106", "title": "Unchecked SUICIDE", "type": "Warning"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 146,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "Anyone can kill this contract and withdraw its balance to their own account.",
+      "function": "kill(address)",
+      "max_gas_used": 263,
+      "min_gas_used": 168,
+      "swc-id": "106",
+      "title": "Unchecked SUICIDE",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -7,9 +7,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "The subtraction can result in an integer underflow.\n",
       "function": "sendeth(address,uint256)",
-      "swc-id": "101",
-      "min_gas_used": 750,
       "max_gas_used": 1035,
+      "min_gas_used": 750,
+      "swc-id": "101",
       "title": "Integer Underflow",
       "type": "Warning"
     },
@@ -19,22 +19,10 @@
       "debug": "<DEBUG-DATA>",
       "description": "The subtraction can result in an integer underflow.\n",
       "function": "sendeth(address,uint256)",
-      "swc-id": "101",
-      "min_gas_used": 1283,
       "max_gas_used": 1758,
-      "title": "Integer Underflow",
-      "type": "Warning"
-    },
-    {
-      "address": 725,
-      "contract": "Unknown",
-      "debug": "<DEBUG-DATA>",
-      "description": "This binary add operation can result in integer overflow.\n",
-      "function": "sendeth(address,uint256)",
+      "min_gas_used": 1283,
       "swc-id": "101",
-      "min_gas_used": 6806,
-      "max_gas_used": 27471,
-      "title": "Integer Overflow",
+      "title": "Integer Underflow",
       "type": "Warning"
     }
   ],

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

@@ -23,15 +23,3 @@ The subtraction can result in an integer underflow.
 ### Description
 
 The subtraction can result in an integer underflow.
-
-## Integer Overflow
-- SWC ID: 101
-- Type: Warning
-- Contract: Unknown
-- Function name: `sendeth(address,uint256)`
-- PC address: 725
-- Estimated Gas Usage: 6806 - 27471
-
-### Description
-
-This binary add operation can result in integer overflow.

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

@@ -20,14 +20,3 @@ The subtraction can result in an integer underflow.
 
 --------------------
 
-==== Integer Overflow ====
-SWC ID: 101
-Type: Warning
-Contract: Unknown
-Function name: sendeth(address,uint256)
-PC address: 725
-Estimated Gas Usage: 6806 - 27471
-This binary add operation can result in integer overflow.
-
---------------------
-

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

@@ -1,46 +1,46 @@
 {
-  "success": true,
-  "error": null,
-  "issues": [
-    {
-      "title": "Dependence on predictable environment variable",
-      "description": "In the function `_function_0xe9874106` the following predictable state variables are used to determine Ether recipient:\n- block.coinbase\n",
-      "function": "_function_0xe9874106",
-      "type": "Warning",
-      "address": 1285,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Ether send",
-      "description": "In the function `_function_0xe9874106` a non-zero amount of Ether is sent to an address taken from storage slot 0.\nThere is a check on storage index 0. This storage slot can be written to by calling the function `fallback`.\n\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-      "function": "_function_0xe9874106",
-      "type": "Warning",
-      "address": 1285,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Exception state",
-      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-      "function": "fallback",
-      "type": "Informational",
-      "address": 356,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Exception state",
-      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-      "function": "_function_0xe9874106",
-      "type": "Informational",
-      "address": 146,
-      "debug": "<DEBUG-DATA>"
-    },
-    {
-      "title": "Transaction order dependence",
-      "description": "A possible transaction order independence vulnerability exists in function _function_0xe9874106. The value or direction of the call statement is determined from a tainted storage location",
-      "function": "_function_0xe9874106",
-      "type": "Warning",
-      "address": 1285,
-      "debug": "<DEBUG-DATA>"
-    }
-  ]
+    "success": true,
+    "error": null,
+    "issues": [
+        {
+            "title": "Dependence on predictable environment variable",
+            "description": "In the function `_function_0xe9874106` the following predictable state variables are used to determine Ether recipient:\n- block.coinbase\n",
+            "function": "_function_0xe9874106",
+            "type": "Warning",
+            "address": 1285,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Ether send",
+            "description": "In the function `_function_0xe9874106` a non-zero amount of Ether is sent to an address taken from storage slot 0.\nThere is a check on storage index 0. This storage slot can be written to by calling the function `fallback`.\n\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+            "function": "_function_0xe9874106",
+            "type": "Warning",
+            "address": 1285,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Exception state",
+            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+            "function": "fallback",
+            "type": "Informational",
+            "address": 356,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Exception state",
+            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+            "function": "_function_0xe9874106",
+            "type": "Informational",
+            "address": 146,
+            "debug": "<DEBUG-DATA>",
+        },
+        {
+            "title": "Transaction order dependence",
+            "description": "A possible transaction order independence vulnerability exists in function _function_0xe9874106. The value or direction of the call statement is determined from a tainted storage location",
+            "function": "_function_0xe9874106",
+            "type": "Warning",
+            "address": 1285,
+            "debug": "<DEBUG-DATA>",
+        },
+    ],
 }