|
|
@ -8,7 +8,7 @@ |
|
|
|
|
|
|
|
|
|
|
|
const MAX_PARALLEL = 4; |
|
|
|
const MAX_PARALLEL = 4; |
|
|
|
|
|
|
|
|
|
|
|
const specs = require(__dirname + '/specs.json'); |
|
|
|
let specs = require(__dirname + '/specs.json'); |
|
|
|
|
|
|
|
|
|
|
|
const proc = require('child_process'); |
|
|
|
const proc = require('child_process'); |
|
|
|
const { PassThrough } = require('stream'); |
|
|
|
const { PassThrough } = require('stream'); |
|
|
@ -20,14 +20,20 @@ if (request.startsWith('-')) { |
|
|
|
extraOptions.unshift(request); |
|
|
|
extraOptions.unshift(request); |
|
|
|
request = ''; |
|
|
|
request = ''; |
|
|
|
} |
|
|
|
} |
|
|
|
const [reqSpec, reqContract] = request.split(':').reverse(); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
for (const { spec, contract, files, options = [] } of Object.values(specs)) { |
|
|
|
if (request) { |
|
|
|
if ((!reqSpec || reqSpec === spec) && (!reqContract || reqContract === contract)) { |
|
|
|
const [reqSpec, reqContract] = request.split(':').reverse(); |
|
|
|
limit(runCertora, spec, contract, files, [...options, ...extraOptions]); |
|
|
|
specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract)); |
|
|
|
|
|
|
|
if (specs.length === 0) { |
|
|
|
|
|
|
|
console.error(`Error: Requested spec '${request}' not found in specs.json`); |
|
|
|
|
|
|
|
process.exit(1); |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
for (const { spec, contract, files, options = [] } of Object.values(specs)) { |
|
|
|
|
|
|
|
limit(runCertora, spec, contract, files, [...options, ...extraOptions]); |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
// Run certora, aggregate the output and print it at the end
|
|
|
|
// Run certora, aggregate the output and print it at the end
|
|
|
|
async function runCertora(spec, contract, files, options = []) { |
|
|
|
async function runCertora(spec, contract, files, options = []) { |
|
|
|
const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options]; |
|
|
|
const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options]; |
|
|
|