cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #8950 from ethereum/smt_external_calls

Browse Source 
[SMTChecker] Support to external calls to unknown code
This commit is contained in:
Leonardo 2020-07-02 10:05:08 +02:00 committed by GitHub
commit b19c1941b7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
21 changed files with 575 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -10,6 +10,8 @@ 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 external calls to unknown code.
Bugfixes:
* NatSpec: Do not consider ``////`` and ``/***`` as NatSpec comments.

152
libsolidity/formal/CHC.cpp
View File

@ -197,8 +197,11 @@ void CHC::endVisit(ContractDefinition const& _contract)
bool CHC::visit(FunctionDefinition const& _function)
{
if (!shouldVisit(_function))
if (!_function.isImplemented())
{
connectBlocks(genesis(), summary(_function));
return false;
}
// This is the case for base constructor inlining.
if (m_currentFunction)
@ -243,7 +246,7 @@ bool CHC::visit(FunctionDefinition const& _function)
void CHC::endVisit(FunctionDefinition const& _function)
{
if (!shouldVisit(_function))
if (!_function.isImplemented())
return;
// This is the case for base constructor inlining.
@ -474,11 +477,14 @@ void CHC::endVisit(FunctionCall const& _funCall)
internalFunctionCall(_funCall);
break;
case FunctionType::Kind::External:
case FunctionType::Kind::BareStaticCall:
externalFunctionCall(_funCall);
SMTEncoder::endVisit(_funCall);
break;
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall:
case FunctionType::Kind::BareStaticCall:
case FunctionType::Kind::Creation:
case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover:
@ -574,6 +580,35 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
m_context.addAssertion(m_error.currentValue() == previousError);
}
void CHC::externalFunctionCall(FunctionCall const& _funCall)
{
solAssert(m_currentContract, "");
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
auto const* function = functionCallToDefinition(_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 ||
function->stateMutability() == StateMutability::View;
if (!usesStaticCall)
for (auto const* var: m_stateVariables)
m_context.variable(*var)->increaseIndex();
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
m_context.addAssertion(nondet);
m_context.addAssertion(m_error.currentValue() == 0);
}
void CHC::unknownFunctionCall(FunctionCall const&)
{
/// Function calls are not handled at the moment,
@ -651,11 +686,6 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
}
}
bool CHC::shouldVisit(FunctionDefinition const& _function) const
{
return _function.isImplemented();
}
void CHC::setCurrentBlock(
smt::SymbolicFunctionVariable const& _block,
vector<smtutil::Expression> const* _arguments
@ -710,10 +740,14 @@ smtutil::SortPointer CHC::constructorSort()
smtutil::SortPointer CHC::interfaceSort()
{
return make_shared<smtutil::FunctionSort>(
m_stateSorts,
smtutil::SortProvider::boolSort
);
solAssert(m_currentContract, "");
return interfaceSort(*m_currentContract);
}
smtutil::SortPointer CHC::nondetInterfaceSort()
{
solAssert(m_currentContract, "");
return nondetInterfaceSort(*m_currentContract);
}
smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
@ -724,6 +758,15 @@ smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
);
}
smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contract)
{
auto sorts = stateSorts(_contract);
return make_shared<smtutil::FunctionSort>(
sorts + sorts,
smtutil::SortProvider::boolSort
);
}
smtutil::SortPointer CHC::arity0FunctionSort()
{
return make_shared<smtutil::FunctionSort>(
@ -802,11 +845,47 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
{
string suffix = base->name() + "_" + to_string(base->id());
m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix);
m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix);
for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
if (!m_context.knownVariable(*var))
createVariable(*var);
/// Base nondeterministic interface that allows
/// 0 steps to be taken, used as base for the inductive
/// rule for each function.
auto const& iface = *m_nondetInterfaces.at(base);
auto state0 = stateVariablesAtIndex(0, *base);
addRule(iface(state0 + state0), "base_nondet");
for (auto const* function: base->definedFunctions())
{
for (auto var: function->parameters())
createVariable(*var);
for (auto var: function->returnParameters())
createVariable(*var);
for (auto const* var: function->localVariables())
createVariable(*var);
m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
if (!base->isLibrary() && !base->isInterface() && !function->isConstructor())
{
auto state1 = stateVariablesAtIndex(1, *base);
auto state2 = stateVariablesAtIndex(2, *base);
auto nondetPre = iface(state0 + state1);
auto nondetPost = iface(state0 + state2);
vector<smtutil::Expression> args{m_error.currentValue()};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
state2 +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
connectBlocks(nondetPre, nondetPost, (*m_summaries.at(base).at(function))(args));
}
}
}
}
@ -842,15 +921,21 @@ smtutil::Expression CHC::summary(ContractDefinition const&)
);
}
smtutil::Expression CHC::summary(FunctionDefinition const& _function)
smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
vector<smtutil::Expression> args{m_error.currentValue()};
auto contract = _function.annotation().contract;
args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables();
args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(_contract);
args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); });
args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(_contract);
args += applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
return (*m_summaries.at(m_currentContract).at(&_function))(args);
return (*m_summaries.at(&_contract).at(&_function))(args);
}
smtutil::Expression CHC::summary(FunctionDefinition const& _function)
{
solAssert(m_currentContract, "");
return summary(_function, *m_currentContract);
}
unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
@ -893,13 +978,18 @@ vector<smtutil::Expression> CHC::initialStateVariables()
return stateVariablesAtIndex(0);
}
vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
vector<smtutil::Expression> CHC::initialStateVariables(ContractDefinition const& _contract)
{
solAssert(m_currentContract, "");
return applyMap(m_stateVariables, [&](auto _var) { return valueAtIndex(*_var, _index); });
return stateVariablesAtIndex(0, _contract);
}
vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index)
{
solAssert(m_currentContract, "");
return stateVariablesAtIndex(_index, *m_currentContract);
}
vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
{
return applyMap(
stateVariablesIncludingInheritedAndPrivate(_contract),
@ -910,7 +1000,12 @@ vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, Contract
vector<smtutil::Expression> CHC::currentStateVariables()
{
solAssert(m_currentContract, "");
return applyMap(m_stateVariables, [this](auto _var) { return currentValue(*_var); });
return currentStateVariables(*m_currentContract);
}
vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
{
return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
}
vector<smtutil::Expression> CHC::currentFunctionVariables()
@ -978,12 +1073,17 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
m_error.increaseIndex();
vector<smtutil::Expression> args{m_error.currentValue()};
auto const* contract = function->annotation().contract;
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
bool otherContract = contract->isLibrary() ||
funType.kind() == FunctionType::Kind::External ||
funType.kind() == FunctionType::Kind::BareStaticCall;
args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
args += otherContract ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
args += symbolicArguments(_funCall);
for (auto const& var: m_stateVariables)
m_context.variable(*var)->increaseIndex();
args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
if (!otherContract)
for (auto const& var: m_stateVariables)
m_context.variable(*var)->increaseIndex();
args += otherContract ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
auto const& returnParams = function->returnParameters();
for (auto param: returnParams)
@ -993,7 +1093,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
createVariable(*param);
args += applyMap(function->returnParameters(), [this](auto _var) { return currentValue(*_var); });
if (contract->isLibrary())
if (otherContract)
return (*m_summaries.at(contract).at(function))(args);
solAssert(m_currentContract, "");

17
libsolidity/formal/CHC.h
View File

@ -77,6 +77,7 @@ private:
void visitAssert(FunctionCall const& _funCall);
void internalFunctionCall(FunctionCall const& _funCall);
void externalFunctionCall(FunctionCall const& _funCall);
void unknownFunctionCall(FunctionCall const& _funCall);
void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
//@}
@ -95,7 +96,6 @@ private:
void resetContractAnalysis();
void eraseKnowledge();
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
bool shouldVisit(FunctionDefinition const& _function) const;
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
@ -106,7 +106,9 @@ private:
static std::vector<smtutil::SortPointer> stateSorts(ContractDefinition const& _contract);
smtutil::SortPointer constructorSort();
smtutil::SortPointer interfaceSort();
smtutil::SortPointer nondetInterfaceSort();
static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const);
smtutil::SortPointer arity0FunctionSort();
smtutil::SortPointer sort(FunctionDefinition const& _function);
smtutil::SortPointer sort(ASTNode const* _block);
@ -149,10 +151,12 @@ private:
/// @returns the symbolic values of the state variables at the beginning
/// of the current transaction.
std::vector<smtutil::Expression> initialStateVariables();
std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index);
std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract);
std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract);
std::vector<smtutil::Expression> stateVariablesAtIndex(int _index);
std::vector<smtutil::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
/// @returns the current symbolic values of the current state variables.
std::vector<smtutil::Expression> currentStateVariables();
std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract);
/// @returns the current symbolic values of the current function's
/// input and output parameters.
@ -173,6 +177,7 @@ private:
smtutil::Expression summary(ContractDefinition const& _contract);
/// @returns a predicate that defines a function summary.
smtutil::Expression summary(FunctionDefinition const& _function);
smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract);
//@}
/// Solver related.
@ -212,6 +217,12 @@ private:
/// Single entry block for all functions.
std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_interfaces;
/// Nondeterministic interfaces.
/// These are used when the analyzed contract makes external calls to unknown code,
/// which means that the analyzed contract can potentially be called
/// nondeterministically.
std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_nondetInterfaces;
/// Artificial Error predicate.
/// Single error block for all assertions.
std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;

20
test/libsolidity/smtCheckerTests/external_calls/external.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
uint x;
D d;
function f() public {
if (x < 10)
++x;
}
function g() public {
d.d();
assert(x < 10);
}
}
// ----
// Warning 4661: (200-214): Assertion violation happens here

29
test/libsolidity/smtCheckerTests/external_calls/external_hash.sol Normal file
View File

@ -0,0 +1,29 @@
pragma experimental SMTChecker;
abstract contract Crypto {
function hash(bytes32) external pure virtual returns (bytes32);
}
contract C {
address owner;
bytes32 sig_1;
bytes32 sig_2;
Crypto d;
constructor() public {
owner = msg.sender;
}
function f1(bytes32 _msg) public {
address prevOwner = owner;
sig_1 = d.hash(_msg);
sig_2 = d.hash(_msg);
assert(prevOwner == owner);
}
function inv() public view {
assert(sig_1 == sig_2);
}
}
// ----
// Warning 4661: (430-452): Assertion violation happens here

31
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol Normal file
View File

@ -0,0 +1,31 @@
pragma experimental SMTChecker;
contract Crypto {
function hash(bytes32) external pure returns (bytes32) {
return bytes32(0);
}
}
contract C {
address owner;
bytes32 sig_1;
bytes32 sig_2;
Crypto d;
constructor() public {
owner = msg.sender;
}
function f1(bytes32 _msg) public {
address prevOwner = owner;
sig_1 = d.hash(_msg);
sig_2 = d.hash(_msg);
assert(prevOwner == owner);
}
function inv() public view {
assert(sig_1 == sig_2);
}
}
// ----
// Warning 4661: (438-460): Assertion violation happens here

38
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol Normal file
View File

@ -0,0 +1,38 @@
pragma experimental SMTChecker;
contract State {
uint x;
function f() public returns (uint) {
if (x == 0) x = 1;
else if (x == 1) x = 2;
else if (x == 2) x = 0;
return x;
}
}
contract C {
address owner;
uint y;
uint z;
State s;
constructor() public {
owner = msg.sender;
}
function f() public {
address prevOwner = owner;
y = s.f();
z = s.f();
assert(prevOwner == owner);
}
function inv() public view {
// This is safe but external calls do not yet support the state
// of the called contract.
assert(owner == address(0) || y != z);
}
}
// ----
// Warning 5084: (551-561): Type conversion is not yet fully supported and might yield false positives.
// Warning 4661: (535-572): Assertion violation happens here

32
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol Normal file
View File

@ -0,0 +1,32 @@
pragma experimental SMTChecker;
contract State {
uint x;
C c;
function f() public view returns (uint) {
return c.g();
}
}
contract C {
address owner;
uint y;
State s;
constructor() public {
owner = msg.sender;
}
function f() public view {
address prevOwner = owner;
uint z = s.f();
assert(z == y);
assert(prevOwner == owner);
}
function g() public view returns (uint) {
return y;
}
}
// ----
// Warning 4661: (306-320): Assertion violation happens here

47
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol Normal file
View File

@ -0,0 +1,47 @@
pragma experimental SMTChecker;
contract Other {
C c;
function h() public {
c.setOwner(address(0));
}
}
contract State {
uint x;
Other o;
C c;
function f() public returns (uint) {
o.h();
return c.g();
}
}
contract C {
address owner;
uint y;
State s;
constructor() public {
owner = msg.sender;
}
function setOwner(address _owner) public {
owner = _owner;
}
function f() public {
address prevOwner = owner;
uint z = s.f();
assert(z == y);
assert(prevOwner == owner);
}
function g() public view returns (uint) {
return y;
}
}
// ----
// Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives.
// Warning 4661: (459-473): Assertion violation happens here
// Warning 4661: (477-503): Assertion violation happens here

39
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol Normal file
View File

@ -0,0 +1,39 @@
pragma experimental SMTChecker;
contract State {
uint x;
C c;
function f() public returns (uint) {
c.setOwner(address(0));
return c.g();
}
}
contract C {
address owner;
uint y;
State s;
constructor() public {
owner = msg.sender;
}
function setOwner(address _owner) public {
owner = _owner;
}
function f() public {
address prevOwner = owner;
uint z = s.f();
assert(z == y);
assert(prevOwner == owner);
}
function g() public view returns (uint) {
return y;
}
}
// ----
// Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives.
// Warning 4661: (388-402): Assertion violation happens here
// Warning 4661: (406-432): Assertion violation happens here

43
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol Normal file
View File

@ -0,0 +1,43 @@
pragma experimental SMTChecker;
contract State {
uint x;
function f() public returns (uint) {
if (x == 0) x = 1;
else if (x == 1) x = 2;
else if (x == 2) x = 0;
return x;
}
}
contract C {
address owner;
uint y;
uint z;
State s;
constructor() public {
owner = msg.sender;
}
function setOwner(address _owner) public {
owner = _owner;
}
function f() public {
address prevOwner = owner;
y = s.f();
z = s.f();
assert(prevOwner == owner);
}
function inv() public view {
// This is safe but external calls do not yet support the state
// of the called contract.
assert(owner == address(0) || y != z);
}
}
// ----
// Warning 4661: (442-468): Assertion violation happens here
// Warning 5084: (617-627): Type conversion is not yet fully supported and might yield false positives.
// Warning 4661: (601-638): Assertion violation happens here

22
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol Normal file
View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
uint x;
D d;
function inc() public {
++x;
}
function f() public {
d.d();
assert(x < 10);
}
}
// ----
// Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (189-203): Assertion violation happens here

28
test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol Normal file
View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
uint x;
uint y;
D d;
function inc2() public {
if (y == 1)
x = 1;
}
function inc1() public {
if (x == 0)
y = 1;
}
function f() public {
uint oldX = x;
d.d();
assert(oldX == x);
}
}
// ----
// Warning 4661: (286-303): Assertion violation happens here

18
test/libsolidity/smtCheckerTests/external_calls/external_safe.sol Normal file
View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
uint x;
D d;
function f() public {
if (x < 10)
++x;
}
function g() public {
d.d();
assert(x < 11);
}
}

26
test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol Normal file
View File

@ -0,0 +1,26 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
uint x;
uint y;
D d;
function inc() public {
if (y == 1)
x = 1;
if (x == 0)
y = 1;
}
function f() public {
uint oldX = x;
d.d();
assert(oldX == x);
}
}
// ----
// Warning 4661: (256-273): Assertion violation happens here

28
test/libsolidity/smtCheckerTests/external_calls/mutex.sol Normal file
View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
uint x;
D d;
bool lock;
modifier mutex {
require(!lock);
lock = true;
_;
lock = false;
}
function set(uint _x) mutex public {
x = _x;
}
function f() mutex public {
uint y = x;
d.d();
assert(y == x);
}
}

30
test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol Normal file
View File

@ -0,0 +1,30 @@
pragma experimental SMTChecker;
abstract contract D {
function d() external virtual;
}
contract C {
uint x;
D d;
bool lock;
modifier mutex {
require(!lock);
lock = true;
_;
lock = false;
}
function set(uint _x) mutex public {
x = _x;
}
function f() public {
uint y = x;
d.d();
assert(y == x);
}
}
// ----
// Warning 4661: (307-321): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
View File

@ -17,4 +17,3 @@ contract C
}
}
// ----
// Warning 4661: (257-271): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/functions/functions_external_3.sol
View File

@ -18,4 +18,3 @@ contract C
}
}
// ----
// Warning 4661: (355-379): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
View File

@ -14,4 +14,6 @@ contract C
}
}
// ----
// Warning 1218: (296-309): Error trying to invoke SMT solver.
// Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning 4661: (296-309): Assertion violation happens here

3
test/libsolidity/smtCheckerTests/types/address_staticcall.sol
View File

@ -20,6 +20,3 @@ contract C
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 4661: (266-281): Assertion violation happens here
// Warning 4661: (285-299): Assertion violation happens here
// Warning 4661: (303-322): Assertion violation happens here
// Warning 4661: (326-350): Assertion violation happens here