Merge pull request #2494 from ethereum/remove-why3

Remove last remains of Why3

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': [

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,

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,

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
-	);
-}
-

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();

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;

libsolidity/interface/Exceptions.h

@@ -60,7 +60,6 @@ public:
 		ParserError,
 		TypeError,
 		SyntaxError,
-		Why3TranslatorError,
 		Warning
 	};
 

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;