From a207d7f44cd661cc647f132230195d58ea22240f Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Thu, 21 Mar 2019 16:25:26 +0100
Subject: [PATCH] [SMTChecker] Add callstack model to overflow checks

---
 libsolidity/formal/SMTChecker.cpp | 5 ++++-
 libsolidity/formal/SMTChecker.h   | 6 ++++--
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index efa29c514..7cdaa49f3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -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);
 	}
 }
 
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 33aeada2c..66f4397e8 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -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()), "");
 		}