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: fixed struct constructor where FixedBytes member is initialized with a string literal

Browse Source
This commit is contained in:
Martin Blicha 2021-05-16 12:56:33 +02:00
parent 1d41ceaed4
commit 9c98ab59f0
3 changed files with 24 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -13,6 +13,7 @@ Compiler Features:
Bugfixes:
* AST: Do not output value of Yul literal if it is not a valid UTF-8 string.
* SMTChecker: Fix internal error on struct constructor with fixed bytes member initialized with string literal.
AST Changes:

10
libsolidity/formal/SMTEncoder.cpp
View File

@ -1158,7 +1158,15 @@ void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall)
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); }));
auto structType = dynamic_cast<StructType const*>(structSymbolicVar.type());
solAssert(structType, "");
auto const& structMembers = structType->structDefinition().members();
solAssert(structMembers.size() == _funCall.sortedArguments().size(), "");
auto args = _funCall.sortedArguments();
structSymbolicVar.assignAllMembers(applyMap(
ranges::views::zip(args, structMembers),
[this] (auto const& argMemberPair) { return expr(*argMemberPair.first, argMemberPair.second->type()); }
));
}
}

14
test/libsolidity/smtCheckerTests/types/struct/struct_constructor_fixed_bytes_from_string_1.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
struct S {
int a;
bytes5 b;
}
function f() public pure {
assert(S({a:2, b:""}).b == bytes5(0)); // should hold
assert(S({a:2, b:""}).a == 0); // should fail
}
}
// ----
// Warning 5523: (0-31): The SMTChecker pragma has been deprecated and will be removed in the future. Please use the "model checker engine" compiler setting to activate the SMTChecker instead. If the pragma is enabled, all engines will be used.
// Warning 6328: (178-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()