From 6606a13ed294fc41401c224b5844d77ee7df0ae1 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 1 Jul 2019 16:16:39 +0200 Subject: [PATCH] [SMTChecker] Remove unsound assertion (too strong) --- libsolidity/formal/SMTEncoder.cpp | 2 -- .../functions/function_call_state_var_init.sol | 13 +++++++++++++ 2 files changed, 13 insertions(+), 2 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 30aa95226..ee09f7e13 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1264,8 +1264,6 @@ SecondarySourceLocation SMTEncoder::callStackMessage(vector cons for (auto const& call: _callStack | boost::adaptors::reversed) if (call.second) callStackLocation.append("", call.second->location()); - // The first function in the tx has no FunctionCall. - solAssert(_callStack.front().second == nullptr, ""); return callStackLocation; } diff --git a/test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol b/test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol new file mode 100644 index 000000000..9044cf99a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + uint x = f(2); + + function f(uint y) internal pure returns (uint) { + assert(y > 1000); + return y; + } +} +// ---- +// Warning: (116-132): Assertion violation happens here +// Warning: (116-132): Assertion violation happens here