From 90c56d9f8e5a83cca5802d5a1ce8c4778989b6ae Mon Sep 17 00:00:00 2001
From: yann300 <yann.levreau@gmail.com>
Date: Wed, 24 May 2017 15:35:25 +0200
Subject: [PATCH] remove formal verification

---
 assets/css/browser-solidity.css |  5 ----
 src/app.js                      |  4 +--
 src/app/analysis-tab.js         | 13 ---------
 src/app/formalVerification.js   | 51 ---------------------------------
 src/app/renderer.js             |  7 +----
 5 files changed, 2 insertions(+), 78 deletions(-)
 delete mode 100644 src/app/formalVerification.js

diff --git a/assets/css/browser-solidity.css b/assets/css/browser-solidity.css
index 7086c4f0fe..b2f62e1982 100644
--- a/assets/css/browser-solidity.css
+++ b/assets/css/browser-solidity.css
@@ -312,11 +312,6 @@ body {
     border: 0 none;
 }
 
-#formalVerificationInput {
-    height: 4.5em;
-    width: 100%;
-}
-
 .contract.hidesub {
     padding-bottom: 0;
     margin: 0;
diff --git a/src/app.js b/src/app.js
index a27fe0a886..6565bb6e83 100644
--- a/src/app.js
+++ b/src/app.js
@@ -21,7 +21,6 @@ var Compiler = require('./app/compiler')
 var ExecutionContext = require('./app/execution-context')
 var UniversalDApp = require('./universal-dapp.js')
 var Debugger = require('./app/debugger')
-var FormalVerification = require('./app/formalVerification')
 var EventManager = require('ethereum-remix').lib.EventManager
 var StaticAnalysis = require('./app/staticanalysis/staticAnalysisView')
 var OffsetToLineColumnConverter = require('./lib/offsetToLineColumnConverter')
@@ -72,7 +71,6 @@ var run = function () {
 
   var executionContext = new ExecutionContext()
   var compiler = new Compiler(handleImportCall)
-  var formalVerification = new FormalVerification($('#verificationView'), compiler.event)
   var offsetToLineColumnConverter = new OffsetToLineColumnConverter(compiler.event)
 
   // return all the files, except the temporary/readonly ones
@@ -772,7 +770,7 @@ var run = function () {
       udapp.getAccounts(callback)
     }
   }
-  var renderer = new Renderer(rendererAPI, formalVerification.event, compiler.event)
+  var renderer = new Renderer(rendererAPI, compiler.event)
 
   // ----------------- StaticAnalysis -----------------
   var staticAnalysisAPI = {
diff --git a/src/app/analysis-tab.js b/src/app/analysis-tab.js
index 810638c1d1..1d72077a96 100644
--- a/src/app/analysis-tab.js
+++ b/src/app/analysis-tab.js
@@ -23,19 +23,6 @@ module.exports = analysisTab
 function analysisTab () {
   return yo`
     <div class="${css.analysisTabView} "id="staticanalysisView">
-      <div class="${css.infoBox}">
-        This tab provides support for <b>formal verification</b> of Solidity contracts.<br>
-        This feature is still in development and thus also not yet well documented,
-        but you can find some information
-        <a href="http://solidity.readthedocs.io/en/latest/security-considerations.html#formal-verification">here</a>.
-        The compiler generates input to be verified
-        (or report errors). Please paste the text below into
-        <a href="http://why3.lri.fr/try/">http://why3.lri.fr/try/</a>
-        to actually perform the verification.
-        We plan to support direct integration in the future.
-      </div>
-      <textarea class="${css.textBox}" id="formalVerificationInput" readonly="readonly"></textarea>
-      <div id="formalVerificationErrors"></div>
     </div>
   `
 }
diff --git a/src/app/formalVerification.js b/src/app/formalVerification.js
deleted file mode 100644
index e56679907d..0000000000
--- a/src/app/formalVerification.js
+++ /dev/null
@@ -1,51 +0,0 @@
-'use strict'
-
-var $ = require('jquery')
-var EventManager = require('ethereum-remix').lib.EventManager
-
-/*
-  trigger compilationFinished
-*/
-function FormalVerification (outputElement, compilerEvent) {
-  this.event = new EventManager()
-  this.outputElement = outputElement
-  var self = this
-  compilerEvent.register('compilationFinished', this, function (success, data, source) {
-    if (success) {
-      self.compilationFinished(data)
-    }
-  })
-  compilerEvent.register('compilationStarted', this, function () {
-    $('#formalVerificationInput', self.outputElement)
-      .val('')
-      .hide()
-    $('#formalVerificationErrors').empty()
-  })
-}
-
-FormalVerification.prototype.compilationFinished = function (compilationResult) {
-  if (compilationResult.formal === undefined) {
-    this.event.trigger(
-      'compilationFinished',
-      [false, 'Formal verification not supported by this compiler version.', $('#formalVerificationErrors'), {noAnnotations: true}]
-    )
-  } else {
-    if (compilationResult.formal['why3'] !== undefined) {
-      $('#formalVerificationInput', this.outputElement).val(
-        '(* copy this to http://why3.lri.fr/try/ *)' +
-        compilationResult.formal['why3']
-      )
-        .show()
-    }
-    if (compilationResult.formal.errors !== undefined) {
-      var errors = compilationResult.formal.errors
-      for (var i = 0; i < errors.length; i++) {
-        this.event.trigger('compilationFinished', [false, errors[i], $('#formalVerificationErrors'), {noAnnotations: true}])
-      }
-    } else {
-      this.event.trigger('compilationFinished', [true, null, null, {noAnnotations: true}])
-    }
-  }
-}
-
-module.exports = FormalVerification
diff --git a/src/app/renderer.js b/src/app/renderer.js
index 294a8c6802..b252e111c4 100644
--- a/src/app/renderer.js
+++ b/src/app/renderer.js
@@ -38,14 +38,9 @@ var css = csjs`
 `
 // ----------------------------------------------
 
-function Renderer (appAPI, formalVerificationEvent, compilerEvent) {
+function Renderer (appAPI, compilerEvent) {
   this.appAPI = appAPI
   var self = this
-  formalVerificationEvent.register('compilationFinished', this, function (success, message, container, options) {
-    if (!success) {
-      self.error(message, container, options)
-    }
-  })
   compilerEvent.register('compilationFinished', this, function (success, data, source) {
     $('#output').empty()
     if (success) {