Skip to content

Commit

Permalink
remove formal verification
Browse files Browse the repository at this point in the history
  • Loading branch information
yann300 committed May 24, 2017
1 parent 6a7159f commit 90c56d9
Show file tree
Hide file tree
Showing 5 changed files with 2 additions and 78 deletions.
5 changes: 0 additions & 5 deletions assets/css/browser-solidity.css
Original file line number Diff line number Diff line change
Expand Up @@ -312,11 +312,6 @@ body {
border: 0 none;
}

#formalVerificationInput {
height: 4.5em;
width: 100%;
}

.contract.hidesub {
padding-bottom: 0;
margin: 0;
Expand Down
4 changes: 1 addition & 3 deletions src/app.js
Original file line number Diff line number Diff line change
Expand Up @@ -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')
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 = {
Expand Down
13 changes: 0 additions & 13 deletions src/app/analysis-tab.js
Original file line number Diff line number Diff line change
Expand Up @@ -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>
`
}
51 changes: 0 additions & 51 deletions src/app/formalVerification.js

This file was deleted.

7 changes: 1 addition & 6 deletions src/app/renderer.js
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down

0 comments on commit 90c56d9

Please sign in to comment.