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

[SMTChecker] Fix ICE on ABI functions with no arguments

Browse Source
This commit is contained in:
Martin Blicha 2021-03-25 12:24:37 +01:00
parent 4080748b1d
commit 5293f05ee3
2 changed files with 26 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libsolidity/formal/SMTEncoder.cpp
View File

@ -775,8 +775,13 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
auto const& args = _funCall.sortedArguments();
auto argsActualLength = kind == FunctionType::Kind::ABIDecode ? 1 : args.size();
vector<smtutil::Expression> symbArgs;
solAssert(inTypes.size() == argsActualLength, "");
if (argsActualLength == 0)
{
defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory()));
return;
}
vector<smtutil::Expression> symbArgs;
for (unsigned i = 0; i < argsActualLength; ++i)
if (args.at(i))
symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));

20
test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
function f() pure public {
bytes memory res = abi.encode();
assert(res.length == 0); // should hold
assert(res.length > 0); // should fail
res = abi.encodePacked();
assert(res.length == 0); // should hold
assert(res.length > 0); // should fail
res = abi.encodeWithSelector(0);
assert(res.length == 4); // should hold, but SMTChecker cannot know this yet
res = abi.encodeWithSignature("");
assert(res.length == 4); // should hold, but SMTChecker cannot know this yet
}
}
// ----
// Warning 6328: (152-174): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (263-285): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (339-362): CHC: Assertion violation happens here.
// Warning 6328: (455-478): CHC: Assertion violation happens here.