run_small.ts

import * as fs from 'fs';
import * as path from 'path';

import solc from './';
import smtchecker from './smtchecker';
import smtsolver from './smtsolver';
          
const settings = { modelChecker: {
  contracts: {
    'a.sol': [ 'C' ]
  },
  divModNoSlacks: true,
  engine: 'chc',
  invariants: [ 'contract', 'reentrancy' ],
  targets: [ 'assert' ],
  solvers: [ 'smtlib2' ]
} };

const sources = {
  'a.sol': {
    'urls': [ './a.sol' ]
  }
};

const basePath = './';

function readFileCallback(path) {
  path = basePath + '/' + path;
  if (fs.existsSync(path)) {
    try {
      return { 'contents': fs.readFileSync(path).toString('utf8') }
    } catch (e) {
      return { error: 'Error reading ' + path + ': ' + e };
    }
  } else
    return { error: 'File not found at ' + path}
}

if (smtsolver.availableSolvers.length === 0) {
  throw 'No solver available, exiting.';
}

let solver;

let eldarica = smtsolver.availableSolvers.filter(
  solver => solver.command === 'eld'
);
if (eldarica.length > 0) {
  solver = eldarica[0];
  // Uncomment to set this solver option.
  //solver.params += ' -abstract:off ';
  // Uncomment to see Eldarica counterexamples.
  // This has *not* been released in SMTChecker.
  //solver.params += ' -cex ';
  // Uncomment to see Eldarica inductive invariants.
  // This has *not* been released in SMTChecker.
  //solver.params += ' -ssol ';
} else {
  solver = smtsolver.availableSolvers[0];
}

console.log('Running with solver ' + solver.name);

const output = JSON.parse(solc.compile(
  JSON.stringify({
    language: 'Solidity',
    sources: sources,
    settings: settings
  }),
  {
    'import': readFileCallback,
    smtSolver: smtchecker.smtCallback(smtsolver.smtSolver, solver)
  }
));

// This just prints the counterexamples without the string quotes.
if (output.errors !== undefined) {
  for (let e in output.errors) {
    if (output.errors[e].errorCode == '6328') {
      console.log(output.errors[e].formattedMessage);
    }
  }
}

// Prints the entire JSON output.
console.log(output);