Merge pull request #559 from ethereum/removeFormalVerification

Remove formal verification

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;

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 = {

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>
   `
 }

src/app/formalVerification.js

@@ -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

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) {