cerc-io/solidity
11
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] Keep knowledge about string literals

Browse Source
This commit is contained in:
Alex Beregszaszi
2020-09-25 11:32:23 +01:00
parent 57e1b2cb92
commit 5090353a1a
7 changed files with 80 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+13
View File
@@ -834,7 +834,20 @@ void SMTEncoder::endVisit(Literal const& _literal)
else if (smt::isBool(type))
defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else if (smt::isStringLiteral(type))
{
createExpr(_literal);
// Add constraints for the length and values as it is known.
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_literal));
solAssert(symbArray, "");
auto value = _literal.value();
m_context.addAssertion(symbArray->length() == value.length());
for (size_t i = 0; i < value.length(); i++)
m_context.addAssertion(
smtutil::Expression::select(symbArray->elements(), i) == size_t(value[i])
);
}
else
{
m_errorReporter.warning(