Merge pull request #2494 from ethereum/remove-why3

Remove last remains of Why3

8 files changed, 2 insertions, 45 deletions

diff --git a/docs/utils/SolidityLexer.py b/docs/utils/SolidityLexer.py
index 1dc99159..ef55c6a2 100644
--- a/docs/utils/SolidityLexer.py
+++ b/docs/utils/SolidityLexer.py
@@ -26,7 +26,7 @@ class SolidityLexer(RegexLexer):
             (r'/\*.*?\*/', Comment.Multiline)
         ],
         'natspec': [
-            (r'@author|@dev|@notice|@return|@param|@why3|@title', Keyword),
+            (r'@author|@dev|@notice|@return|@param|@title', Keyword),
             (r'.[^@*\n]*?', Comment.Special)
         ],
         'docstringsingle': [
diff --git a/libsolidity/analysis/DocStringAnalyser.cpp b/libsolidity/analysis/DocStringAnalyser.cpp
index 6a8fa08e..9a846b31 100644
--- a/libsolidity/analysis/DocStringAnalyser.cpp
+++ b/libsolidity/analysis/DocStringAnalyser.cpp
@@ -40,7 +40,7 @@ bool DocStringAnalyser::analyseDocStrings(SourceUnit const& _sourceUnit)
 
 bool DocStringAnalyser::visit(ContractDefinition const& _node)
 {
-	static const set<string> validTags = set<string>{"author", "title", "dev", "notice", "why3"};
+	static const set<string> validTags = set<string>{"author", "title", "dev", "notice"};
 	parseDocStrings(_node, _node.annotation(), validTags, "contracts");
 
 	return true;
@@ -66,16 +66,6 @@ bool DocStringAnalyser::visit(EventDefinition const& _node)
 	return true;
 }
 
-bool DocStringAnalyser::visitNode(ASTNode const& _node)
-{
-	if (auto node = dynamic_cast<Statement const*>(&_node))
-	{
-		static const set<string> validTags = {"why3"};
-		parseDocStrings(*node, node->annotation(), validTags, "statements");
-	}
-	return true;
-}
-
 void DocStringAnalyser::handleCallable(
 	CallableDeclaration const& _callable,
 	Documented const& _node,
diff --git a/libsolidity/analysis/DocStringAnalyser.h b/libsolidity/analysis/DocStringAnalyser.h
index e871cb60..158b4060 100644
--- a/libsolidity/analysis/DocStringAnalyser.h
+++ b/libsolidity/analysis/DocStringAnalyser.h
@@ -48,8 +48,6 @@ private:
 	virtual bool visit(ModifierDefinition const& _modifier) override;
 	virtual bool visit(EventDefinition const& _event) override;
 
-	virtual bool visitNode(ASTNode const&) override;
-
 	void handleCallable(
 		CallableDeclaration const& _callable,
 		Documented const& _node,
diff --git a/libsolidity/interface/ErrorReporter.cpp b/libsolidity/interface/ErrorReporter.cpp
index 2cbb952c..6e2667a5 100644
--- a/libsolidity/interface/ErrorReporter.cpp
+++ b/libsolidity/interface/ErrorReporter.cpp
@@ -165,22 +165,3 @@ void ErrorReporter::docstringParsingError(string const& _description)
 		_description
 	);
 }
-
-void ErrorReporter::why3TranslatorError(ASTNode const& _location, std::string const& _description)
-{
-	error(
-		Error::Type::Why3TranslatorError,
-		_location.location(),
-		_description
-	);
-}
-
-void ErrorReporter::fatalWhy3TranslatorError(ASTNode const& _location, std::string const& _description)
-{
-	fatalError(
-		Error::Type::Why3TranslatorError,
-		_location.location(),
-		_description
-	);
-}
-
diff --git a/libsolidity/interface/ErrorReporter.h b/libsolidity/interface/ErrorReporter.h
index 83324446..e5605d24 100644
--- a/libsolidity/interface/ErrorReporter.h
+++ b/libsolidity/interface/ErrorReporter.h
@@ -79,10 +79,6 @@ public:
 
 	void docstringParsingError(std::string const& _location);
 
-	void why3TranslatorError(ASTNode const& _location, std::string const& _description);
-
-	void fatalWhy3TranslatorError(ASTNode const& _location, std::string const& _description);
-
 	ErrorList const& errors() const;
 
 	void clear();
diff --git a/libsolidity/interface/Exceptions.cpp b/libsolidity/interface/Exceptions.cpp
index deee92aa..9f2a2d06 100644
--- a/libsolidity/interface/Exceptions.cpp
+++ b/libsolidity/interface/Exceptions.cpp
@@ -46,9 +46,6 @@ Error::Error(Type _type, SourceLocation const& _location, string const& _descrip
 	case Type::TypeError:
 		m_typeName = "TypeError";
 		break;
-	case Type::Why3TranslatorError:
-		m_typeName = "Why3TranslatorError";
-		break;
 	case Type::Warning:
 		m_typeName = "Warning";
 		break;
diff --git a/libsolidity/interface/Exceptions.h b/libsolidity/interface/Exceptions.h
index 5fdb8f11..09301b10 100644
--- a/libsolidity/interface/Exceptions.h
+++ b/libsolidity/interface/Exceptions.h
@@ -60,7 +60,6 @@ public:
 		ParserError,
 		TypeError,
 		SyntaxError,
-		Why3TranslatorError,
 		Warning
 	};
 
diff --git a/solc/jsonCompiler.cpp b/solc/jsonCompiler.cpp
index 1d31ea30..adf991d6 100644
--- a/solc/jsonCompiler.cpp
+++ b/solc/jsonCompiler.cpp
@@ -164,10 +164,6 @@ string compile(StringMap const& _sources, bool _optimize, CStyleReadFileCallback
 	//       "srcmapRuntime" = "0:1:2",
 	//       "assembly" = {}
 	//     }
-	//   },
-	//   "formal": {
-	//     "errors": [ "Error 1" ],
-	//     "why3": "why3 source"
 	//   }
 	// }
 	Json::Value output = Json::objectValue;