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 internal error on constructor of a recursive struct

Browse Source
This commit is contained in:
Martin Blicha 2020-12-15 09:15:59 +01:00
parent d83ce0bcdd
commit e2c27b8ea4
3 changed files with 40 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/formal/SMTEncoder.cpp
View File

@ -1144,8 +1144,12 @@ void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier)
void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall)
{
solAssert(*_funCall.annotation().kind == FunctionCallKind::StructConstructorCall, "");
auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
structSymbolicVar.assignAllMembers(applyMap(_funCall.sortedArguments(), [this](auto const& arg) { return expr(*arg); }));
if (smt::isNonRecursiveStruct(*_funCall.annotation().type))
{
auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
structSymbolicVar.assignAllMembers(applyMap(_funCall.sortedArguments(), [this](auto const& arg) { return expr(*arg); }));
}
}
void SMTEncoder::endVisit(Literal const& _literal)

13
test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_1.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract Test {
struct RecursiveStruct {
RecursiveStruct[] vals;
}
function func() public pure {
RecursiveStruct[1] memory val = [ RecursiveStruct(new RecursiveStruct[](42)) ];
}
}
// ----
// Warning 2072: (136-165): Unused local variable.
// Warning 8364: (170-212): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
// Warning 8364: (170-212): Assertion checker does not yet implement type struct Test.RecursiveStruct memory

21
test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_2.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract Test {
struct RecursiveStruct {
uint x;
RecursiveStruct[] vals;
}
function func() public pure {
RecursiveStruct memory val = RecursiveStruct(1, new RecursiveStruct[](42));
assert(val.x == 1);
}
}
// ----
// Warning 8115: (146-172): Assertion checker does not yet support the type of this variable.
// Warning 8364: (175-220): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
// Warning 7650: (231-236): Assertion checker does not yet support this expression.
// Warning 8364: (231-234): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
// Warning 6328: (224-242): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nfunc()
// Warning 8115: (146-172): Assertion checker does not yet support the type of this variable.
// Warning 8364: (175-220): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
// Warning 7650: (231-236): Assertion checker does not yet support this expression.
// Warning 8364: (231-234): Assertion checker does not yet implement type struct Test.RecursiveStruct memory