From 555dc4f46fae9da72aaff70059686aa34172910b Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Tue, 30 May 2017 09:17:02 +0100
Subject: Remove Why3 generator

---
 solc/CommandLineInterface.cpp | 19 ++-----------------
 1 file changed, 2 insertions(+), 17 deletions(-)

(limited to 'solc')

diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp
index 0dbedd3c..d0134113 100644
--- a/solc/CommandLineInterface.cpp
+++ b/solc/CommandLineInterface.cpp
@@ -37,7 +37,6 @@
 #include <libsolidity/interface/SourceReferenceFormatter.h>
 #include <libsolidity/interface/GasEstimator.h>
 #include <libsolidity/interface/AssemblyStack.h>
-#include <libsolidity/formal/Why3Translator.h>
 
 #include <libevmasm/Instruction.h>
 #include <libevmasm/GasMeter.h>
@@ -393,17 +392,6 @@ void CommandLineInterface::handleGasEstimation(string const& _contract)
 	}
 }
 
-void CommandLineInterface::handleFormal()
-{
-	if (!m_args.count(g_argFormal))
-		return;
-
-	if (m_args.count(g_argOutputDir))
-		createFile("solidity.mlw", m_compiler->formalTranslation());
-	else
-		cout << "Formal version:" << endl << m_compiler->formalTranslation() << endl;
-}
-
 void CommandLineInterface::readInputFilesAndConfigureRemappings()
 {
 	bool addStdin = false;
@@ -790,10 +778,6 @@ bool CommandLineInterface::processInput()
 		unsigned runs = m_args[g_argOptimizeRuns].as<unsigned>();
 		bool successful = m_compiler->compile(optimize, runs, m_libraries);
 
-		if (successful && m_args.count(g_argFormal))
-			if (!m_compiler->prepareFormalAnalysis())
-				successful = false;
-
 		for (auto const& error: m_compiler->errors())
 			SourceReferenceFormatter::printExceptionInformation(
 				cerr,
@@ -1185,7 +1169,8 @@ void CommandLineInterface::outputCompilationResults()
 		handleNatspec(DocumentationType::NatspecUser, contract);
 	} // end of contracts iteration
 
-	handleFormal();
+	if (m_args.count(g_argFormal))
+		cerr << "Support for the Why3 output was removed." << endl;
 }
 
 }
-- 
cgit