Do not trust code of external functions

This commit is contained in:
Leonardo Alt 2020-07-01 18:19:56 +02:00
parent 56e7d43384
commit 5517e817d5
4 changed files with 7 additions and 2 deletions

View File

@ -10,7 +10,7 @@ Compiler Features:
* Commandline Interface: Prevent some incompatible commandline options from being used together.
* NatSpec: Support NatSpec comments on events.
* Yul Optimizer: Store knowledge about storage / memory after ``a := sload(x)`` / ``a := mload(x)``.
* SMTChecker: Support to external calls to unknown code and to known view/pure functions.
* SMTChecker: Support external calls to unknown code.
Bugfixes:

View File

@ -592,6 +592,9 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
if (!function)
return;
for (auto var: function->returnParameters())
m_context.variable(*var)->increaseIndex();
auto preCallState = currentStateVariables();
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
function->stateMutability() == StateMutability::Pure ||
@ -602,7 +605,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
m_context.addAssertion(nondet);
m_context.addAssertion(predicate(_funCall));
m_context.addAssertion(m_error.currentValue() == 0);
}

View File

@ -27,3 +27,5 @@ contract C {
assert(sig_1 == sig_2);
}
}
// ----
// Warning 4661: (438-460): Assertion violation happens here

View File

@ -16,3 +16,4 @@ contract D
}
}
// ----
// Warning 4661: (191-206): Assertion violation happens here