cerc-io/solidity
15
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] Add callstack model to overflow checks

Browse Source
This commit is contained in:
Leonardo Alt 2019-03-21 16:25:26 +01:00
parent 939a178193
commit a207d7f44c
2 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/SMTChecker.cpp
View File

@ -389,7 +389,8 @@ void SMTChecker::addOverflowTarget(
std::move(_intType),
std::move(_value),
currentPathConditions(),
_location
_location,
m_callStack
);
}
@ -397,10 +398,12 @@ void SMTChecker::checkUnderOverflow()
{
for (auto& target: m_overflowTargets)
{
swap(m_callStack, target.callStack);
if (target.type != OverflowTarget::Type::Overflow)
checkUnderflow(target);
if (target.type != OverflowTarget::Type::Underflow)
checkOverflow(target);
swap(m_callStack, target.callStack);
}
}

6
libsolidity/formal/SMTChecker.h
View File

@ -154,13 +154,15 @@ private:
smt::Expression value;
smt::Expression path;
langutil::SourceLocation const& location;
std::vector<ASTNode const*> callStack;
OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location):
OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location, std::vector<ASTNode const*> _callStack):
type(_type),
intType(_intType),
value(_value),
path(_path),
location(_location)
location(_location),
callStack(move(_callStack))
{
solAssert(dynamic_cast<IntegerType const*>(intType.get()), "");
}