Remove Why3 generator

2 files changed, 0 insertions, 22 deletions

diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 8be2c8dd..e2507821 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -40,7 +40,6 @@
 #include <libsolidity/interface/ABI.h>
 #include <libsolidity/interface/Natspec.h>
 #include <libsolidity/interface/GasEstimator.h>
-#include <libsolidity/formal/Why3Translator.h>
 
 #include <libevmasm/Exceptions.h>
 
@@ -316,20 +315,6 @@ void CompilerStack::link()
 	}
 }
 
-bool CompilerStack::prepareFormalAnalysis(ErrorReporter* _errorReporter)
-{
-	if (!_errorReporter)
-		_errorReporter = &m_errorReporter;
-	Why3Translator translator(*_errorReporter);
-	for (Source const* source: m_sourceOrder)
-		if (!translator.process(*source->ast))
-			return false;
-
-	m_formalTranslation = translator.translation();
-
-	return true;
-}
-
 eth::AssemblyItems const* CompilerStack::assemblyItems(string const& _contractName) const
 {
 	Contract const& currentContract = contract(_contractName);
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index f7435f0e..c51ae9c9 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -129,12 +129,6 @@ public:
 	/// @returns false on error.
 	bool compile(std::string const& _sourceCode, bool _optimize = false, unsigned _runs = 200);
 
-	/// Tries to translate all source files into a language suitable for formal analysis.
-	/// @param _errors list to store errors - defaults to the internal error list.
-	/// @returns false on error.
-	bool prepareFormalAnalysis(ErrorReporter* _errorReporter = nullptr);
-	std::string const& formalTranslation() const { return m_formalTranslation; }
-
 	/// @returns the assembled object for a contract.
 	eth::LinkerObject const& object(std::string const& _contractName = "") const;
 	/// @returns the runtime object for the contract.
@@ -290,7 +284,6 @@ private:
 	std::map<ASTNode const*, std::shared_ptr<DeclarationContainer>> m_scopes;
 	std::vector<Source const*> m_sourceOrder;
 	std::map<std::string const, Contract> m_contracts;
-	std::string m_formalTranslation;
 	ErrorList m_errorList;
 	ErrorReporter m_errorReporter;
 	bool m_metadataLiteralSources = false;