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

Merge pull request #6008 from ethereum/smt_fix_abstract_assignment

Browse Source 
[SMTChecker] Assert type is not function when assigning
This commit is contained in:
chriseth 2019-02-18 14:54:20 +01:00 committed by GitHub
commit cb0ad2266c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 25 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/SMTChecker.cpp
View File

@ -1371,7 +1371,7 @@ void SMTChecker::createExpr(Expression const& _e)
void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
{ {
createExpr(_e); createExpr(_e);
solAssert(isSupportedType(*_e.annotation().type), "Equality operator applied to type that is not fully supported"); solAssert(smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
m_interface->addAssertion(expr(_e) == _value); m_interface->addAssertion(expr(_e) == _value);
} }

24
test/libsolidity/smtCheckerTests/types/struct_1.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C
{
struct S {
uint x;
}
mapping (uint => S) smap;
function f(uint y, uint v) public {
smap[y] = S(v);
S memory smem = S(v);
}
}
// ----
// Warning: (157-170): Unused local variable.
// Warning: (157-170): Assertion checker does not yet support the type of this variable.
// Warning: (139-146): Assertion checker does not yet implement this type.
// Warning: (149-153): Assertion checker does not yet implement this expression.
// Warning: (139-153): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (173-177): Assertion checker does not yet implement this expression.
// Warning: (173-177): Internal error: Expression undefined for SMT solver.
// Warning: (173-177): Assertion checker does not yet implement this type.