Preliminary why3 code output.

4 files changed, 41 insertions, 19 deletions

diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 6b55b408..18eec0a2 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -32,6 +32,7 @@
 #include <libsolidity/codegen/Compiler.h>
 #include <libsolidity/interface/CompilerStack.h>
 #include <libsolidity/interface/InterfaceHandler.h>
+#include <libsolidity/formal/Why3Translator.h>
 
 #include <libdevcore/SHA3.h>
 
@@ -205,6 +206,18 @@ void CompilerStack::link(const std::map<string, h160>& _libraries)
 	}
 }
 
+bool CompilerStack::prepareFormalAnalysis()
+{
+	Why3Translator translator(m_errors);
+	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 ac71da2e..0473d58b 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -108,6 +108,11 @@ public:
 	/// Inserts the given addresses into the linker objects of all compiled contracts.
 	void link(std::map<std::string, h160> const& _libraries);
 
+	/// Tries to translate all source files into a language suitable for formal analysis.
+	/// @returns false on error.
+	bool prepareFormalAnalysis();
+	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.
@@ -167,7 +172,6 @@ public:
 	/// @returns the list of errors that occured during parsing and type checking.
 	ErrorList const& errors() const { return m_errors; }
 
-
 private:
 	/**
 	 * Information pertaining to one source unit, filled gradually during parsing and compilation.
@@ -211,6 +215,7 @@ private:
 	std::shared_ptr<GlobalContext> m_globalContext;
 	std::vector<Source const*> m_sourceOrder;
 	std::map<std::string const, Contract> m_contracts;
+	std::string m_formalTranslation;
 	ErrorList m_errors;
 };
 
diff --git a/libsolidity/interface/Exceptions.cpp b/libsolidity/interface/Exceptions.cpp
index 2e79ab39..84d4d108 100644
--- a/libsolidity/interface/Exceptions.cpp
+++ b/libsolidity/interface/Exceptions.cpp
@@ -30,23 +30,26 @@ Error::Error(Type _type): m_type(_type)
 {
 	switch(m_type)
 	{
-		case Type::DeclarationError:
-			m_typeName = "Declaration Error";
-			break;
-		case Type::DocstringParsingError:
-			m_typeName = "Docstring Parsing Error";
-			break;
-		case Type::ParserError:
-			m_typeName = "Parser Error";
-			break;
-		case Type::TypeError:
-			m_typeName = "Type Error";
-			break;
-		case Type::Warning:
-			m_typeName = "Warning";
-			break;
-		default:
-			solAssert(false, "");
-			break;
+	case Type::DeclarationError:
+		m_typeName = "Declaration Error";
+		break;
+	case Type::DocstringParsingError:
+		m_typeName = "Docstring Parsing Error";
+		break;
+	case Type::ParserError:
+		m_typeName = "Parser Error";
+		break;
+	case Type::TypeError:
+		m_typeName = "Type Error";
+		break;
+	case Type::FormalError:
+		m_typeName = "Formal Error";
+		break;
+	case Type::Warning:
+		m_typeName = "Warning";
+		break;
+	default:
+		solAssert(false, "");
+		break;
 	}
 }
diff --git a/libsolidity/interface/Exceptions.h b/libsolidity/interface/Exceptions.h
index cda6b97e..830ec286 100644
--- a/libsolidity/interface/Exceptions.h
+++ b/libsolidity/interface/Exceptions.h
@@ -47,6 +47,7 @@ public:
 		DocstringParsingError,
 		ParserError,
 		TypeError,
+		FormalError,
 		Warning
 	};