cerc-io/solidity
10
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 constraints of string literals after assignment

Browse Source
This commit is contained in:
Alex Beregszaszi 2020-09-25 10:34:18 +01:00
parent 5090353a1a
commit 9c1b041dcb
6 changed files with 4 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -5,7 +5,7 @@ Language Features:
Compiler Features: Compiler Features:
* Export compiler-generated utility sources via standard-json or combined-json. * Export compiler-generated utility sources via standard-json or combined-json.
* SMTChecker: Keep knowledge about string literals and thus support the ``.length`` property properly. * SMTChecker: Keep knowledge about string literals, even through assignment, and thus support the ``.length`` property properly.
* SMTChecker: Support events and low-level logs. * SMTChecker: Support events and low-level logs.
* SMTChecker: Support ``revert()``. * SMTChecker: Support ``revert()``.
* SMTChecker: Support shifts. * SMTChecker: Support shifts.

2
libsolidity/formal/SMTEncoder.cpp
View File

@ -1690,9 +1690,7 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression con
// This is a special case where the SMT sorts are different. // This is a special case where the SMT sorts are different.
// For now we are unaware of other cases where this happens, but if they do appear // For now we are unaware of other cases where this happens, but if they do appear
// we should extract this into an `implicitConversion` function. // we should extract this into an `implicitConversion` function.
if (_variable.type()->category() != Type::Category::Array || _value.annotation().type->category() != Type::Category::StringLiteral)
assignment(_variable, expr(_value, _variable.type())); assignment(_variable, expr(_value, _variable.type()));
// TODO else { store each string literal byte into the array }
} }
void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value) void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)

2
test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
View File

@ -10,4 +10,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (161-181): Assertion violation happens here. // Warning 6328: (215-235): Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol
View File

@ -11,5 +11,4 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (164-184): Assertion violation happens here. // Warning 6328: (248-268): Assertion violation happens here.
// Warning 6328: (194-214): Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/types/bytes_length.sol
View File

@ -11,4 +11,3 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (106-127): Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/types/string_length.sol
View File

@ -16,6 +16,3 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (111-140): Assertion violation happens here.
// Warning 6328: (217-246): Assertion violation happens here.
// Warning 6328: (353-382): Assertion violation happens here.