From 9b64dc501da5c743b948e4dca844a6cd67766be1 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leonardoaltt@gmail.com>
Date: Mon, 12 Mar 2018 20:15:27 +0100
Subject: [PATCH] [SMTChecker_Bool] Fix PR review comments: method renaming and
 solAssert

---
 libsolidity/formal/SMTChecker.cpp  | 15 ++++++++-------
 libsolidity/formal/SSAVariable.cpp | 12 ++++++------
 libsolidity/formal/SSAVariable.h   |  6 +++---
 3 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index d4f94f16c..8f4abdc27 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -205,7 +205,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 			_assignment.location(),
 			"Assertion checker does not yet implement compound assignment."
 		);
-	else if (!SSAVariable::supportedType(_assignment.annotation().type->category()))
+	else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category()))
 		m_errorReporter.warning(
 			_assignment.location(),
 			"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
@@ -266,7 +266,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	{
 	case Token::Not: // !
 	{
-		solAssert(SSAVariable::typeBool(_op.annotation().type->category()), "");
+		solAssert(SSAVariable::isBool(_op.annotation().type->category()), "");
 		defineExpr(_op, !expr(_op.subExpression()));
 		break;
 	}
@@ -274,7 +274,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	case Token::Dec: // -- (pre- or postfix)
 	{
 
-		solAssert(SSAVariable::typeInteger(_op.annotation().type->category()), "");
+		solAssert(SSAVariable::isInteger(_op.annotation().type->category()), "");
 		solAssert(_op.subExpression().annotation().lValueRequested, "");
 		if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
 		{
@@ -371,7 +371,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	{
 		// Will be translated as part of the node that requested the lvalue.
 	}
-	else if (SSAVariable::supportedType(_identifier.annotation().type->category()))
+	else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
 		defineExpr(_identifier, currentValue(*decl));
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
@@ -445,13 +445,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 void SMTChecker::compareOperation(BinaryOperation const& _op)
 {
 	solAssert(_op.annotation().commonType, "");
-	if (SSAVariable::supportedType(_op.annotation().commonType->category()))
+	if (SSAVariable::isSupportedType(_op.annotation().commonType->category()))
 	{
 		smt::Expression left(expr(_op.leftExpression()));
 		smt::Expression right(expr(_op.rightExpression()));
 		Token::Value op = _op.getOperator();
 		shared_ptr<smt::Expression> value;
-		if (SSAVariable::typeInteger(_op.annotation().commonType->category()))
+		if (SSAVariable::isInteger(_op.annotation().commonType->category()))
 		{
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
@@ -464,6 +464,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
 		}
 		else // Bool
 		{
+			solAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "");
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
 				op == Token::NotEqual ? (left != right) :
@@ -744,7 +745,7 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
 
 bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
-	if (SSAVariable::supportedType(_varDecl.type()->category()))
+	if (SSAVariable::isSupportedType(_varDecl.type()->category()))
 	{
 		solAssert(m_variables.count(&_varDecl) == 0, "");
 		m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index 3f2a61f1d..f3213e03c 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -33,9 +33,9 @@ SSAVariable::SSAVariable(
 {
 	resetIndex();
 
-	if (typeInteger(_decl.type()->category()))
+	if (isInteger(_decl.type()->category()))
 		m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
-	else if (typeBool(_decl.type()->category()))
+	else if (isBool(_decl.type()->category()))
 		m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
 	else
 	{
@@ -43,17 +43,17 @@ SSAVariable::SSAVariable(
 	}
 }
 
-bool SSAVariable::supportedType(Type::Category _category)
+bool SSAVariable::isSupportedType(Type::Category _category)
 {
-	return typeInteger(_category) || typeBool(_category);
+	return isInteger(_category) || isBool(_category);
 }
 
-bool SSAVariable::typeInteger(Type::Category _category)
+bool SSAVariable::isInteger(Type::Category _category)
 {
 	return _category == Type::Category::Integer;
 }
 
-bool SSAVariable::typeBool(Type::Category _category)
+bool SSAVariable::isBool(Type::Category _category)
 {
 	return _category == Type::Category::Bool;
 }
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index 7e2ebc8c4..bf5dae3b5 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -69,9 +69,9 @@ public:
 	void setUnknownValue();
 
 	/// So far Int and Bool are supported.
-	static bool supportedType(Type::Category _category);
-	static bool typeInteger(Type::Category _category);
-	static bool typeBool(Type::Category _category);
+	static bool isSupportedType(Type::Category _category);
+	static bool isInteger(Type::Category _category);
+	static bool isBool(Type::Category _category);
 
 private:
 	smt::Expression valueAtSequence(int _seq) const