aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/interface/CompilerStack.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/interface/CompilerStack.cpp')
-rw-r--r--libsolidity/interface/CompilerStack.cpp13
1 files changed, 13 insertions, 0 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);