From 02f4884f9ef9cdface89bc8cf4a514ed73af94cb Mon Sep 17 00:00:00 2001 From: Mak Nazecic-Andrlon Date: Mon, 17 Dec 2018 15:16:03 +1100 Subject: [PATCH] Add package.json and fix README.md --- .gitignore | 1 + README.md | 42 +++-- lib/analysis.js | 28 +-- package-lock.json | 421 +++++++++++++++++++++++++++++++++++++++++++ package.json | 37 ++++ test/testExamples.js | 6 +- 6 files changed, 500 insertions(+), 35 deletions(-) create mode 100644 package-lock.json create mode 100644 package.json diff --git a/.gitignore b/.gitignore index 58644f3..c516ff7 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,4 @@ solver_commands.smt2 data.dzn model.fzn model.mzn +node_modules diff --git a/README.md b/README.md index 4af9b92..94bd3e2 100644 --- a/README.md +++ b/README.md @@ -1,28 +1,32 @@ -# Concolic analysis for Jalangi 2 +# Aratha -This is a prototype concolic analysis tool for Jalangi 2. To run it, you require -a working copy of either the [CVC4](http://cvc4.cs.stanford.edu/) or the -[Z3](https://github.com/Z3Prover/z3) SMT solver and Node.js v7 or up, as well as -a working setup of Jalangi 2. +Aratha is a prototype dynamic symbolic execution tool for JavaScript built on +[Jalangi 2](https://github.com/Samsung/jalangi2). To run it, you require +a working copy of the [G-Strings](https://bitbucket.org/robama/g-strings.git) CP +solver, or one of the SMT solvers [CVC4](http://cvc4.cs.stanford.edu/) or +[Z3](https://github.com/Z3Prover/z3), as well as Node v7 or higher. -## How to run the analysis - -The default solver is CVC4, and the environment variable `CVC4_PATH` must be set -to the path to CVC4, if it is not in your `PATH`. - -Alternatively, you can set `SMT_SOLVER=z3`to use Z3 instead. In this case, -`Z3_PATH` must point to Z3 (or `z3` must be in your `PATH`). - -To analyze a script, run +## Running the analysis +First, install the dependencies by running ``` -node ../src/js/commands/jalangi.js --analysis ./ +$ npm install +``` +from this directory. To analyze a script, run +``` +$ npm run analyze -- ``` - from this directory. -## Running tests +### Options + +The default solver is CVC4, and the environment variable `CVC4_PATH` must be set +to the path to CVC4 if `cvc4` is not in your `PATH`. + +Alternatively, you can set `SOLVER=z3`to use Z3 instead. In this case, +`Z3_PATH` must point to Z3 (or `z3` must be in your `PATH`). + +## Tests The tests are written with [Mocha](https://mochajs.org/). To run them, run -`mocha` from this directory, or `../node_modules/.bin/mocha` if you've installed -Jalangi 2's dependencies. +`npm test` from this directory. diff --git a/lib/analysis.js b/lib/analysis.js index 43b698b..1ab4f13 100644 --- a/lib/analysis.js +++ b/lib/analysis.js @@ -21,7 +21,7 @@ 'abort': false, 'verifyModel': false } - + const path = require("path"); const process = require("process"); const fs = require("fs"); @@ -126,8 +126,8 @@ break; default: throw new Error(`invalid solver ${SOLVER}`); - } - + } + if (solver.isCPSolver()) { if (process.env.INCREMENTAL === "0") console.error("Warning: incremental option disabled for CP solvers."); @@ -172,7 +172,7 @@ const dseOptions = { unsatCores: process.env.UNSAT_CORES === "1", - incremental: !(process.env.SOLVER === "G-Strings") && + incremental: !(process.env.SOLVER === "G-Strings") && !(process.env.INCREMENTAL === "0"), }; @@ -200,7 +200,7 @@ const value = this.conditional(null, cond); return value ? value.result : cond; }; - + sandbox.assert = (cond) => { if(!sandbox.check(cond)) { throw new ProcessExitException("J$.assert(): failed"); @@ -234,19 +234,21 @@ let first = true; try { fs.writeSync(inputLog, "[\n"); - const searcher = new DSE(solver, (newInput) => { + const searcher = new DSE(solver, (newInput) => { if (!first) { fs.writeSync(inputLog, ",\n"); } first = false; - var isCircular = require('is-circular'); - if (isCircular(newInput)) { - console.log("Warning! Circular object detected. Ignored input") - } - else { - fs.writeSync(inputLog, JSON.stringify(newInput)); + let serializedInput = null; + try { + serializedInput = JSON.stringify(newInput); + } catch(e) { + console.warn("Circular object detected; omitting from output log"); + } + if (serializedInput !== null) { + fs.writeSync(inputLog, serializedInput); fs.fsyncSync(inputLog); - } + } this.inputs = newInput; this.path = new ExecutionPath(); resetNameCounter(); diff --git a/package-lock.json b/package-lock.json new file mode 100644 index 0000000..da2cca4 --- /dev/null +++ b/package-lock.json @@ -0,0 +1,421 @@ +{ + "name": "aratha", + "version": "0.0.1", + "lockfileVersion": 1, + "requires": true, + "dependencies": { + "acorn": { + "version": "3.1.0", + "resolved": "http://registry.npmjs.org/acorn/-/acorn-3.1.0.tgz", + "integrity": "sha1-55ooHCOYPMwHlHGoSYZgZ+fwxpM=" + }, + "argparse": { + "version": "0.1.6", + "resolved": "https://registry.npmjs.org/argparse/-/argparse-0.1.6.tgz", + "integrity": "sha1-Q01M6vdydeEX05YpPcspd8MbQOw=", + "requires": { + "underscore": "~1.3.3", + "underscore.string": "~2.1.1" + } + }, + "balanced-match": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.0.tgz", + "integrity": "sha1-ibTRmasr7kneFk6gK4nORi1xt2c=", + "dev": true + }, + "brace-expansion": { + "version": "1.1.11", + "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz", + "integrity": "sha512-iCuPHDFgrHX7H2vEI/5xpz07zSHB00TpugqhmYtVmMO6518mCuRMoOYFldEBl0g187ufozdaHgWKcYFb61qGiA==", + "dev": true, + "requires": { + "balanced-match": "^1.0.0", + "concat-map": "0.0.1" + } + }, + "browser-stdout": { + "version": "1.3.1", + "resolved": "https://registry.npmjs.org/browser-stdout/-/browser-stdout-1.3.1.tgz", + "integrity": "sha512-qhAVI1+Av2X7qelOfAIYwXONood6XlZE/fXaBSmW/T5SzLAmCgzi+eiWE7fUvbHaeNBQH13UftjpXxsfLkMpgw==", + "dev": true + }, + "cli-table": { + "version": "0.0.2", + "resolved": "https://registry.npmjs.org/cli-table/-/cli-table-0.0.2.tgz", + "integrity": "sha1-mChn4WQ1Mlxmwgih5xuVM26jCTs=", + "requires": { + "colors": "0.3.0" + } + }, + "codemirror": { + "version": "5.1.0", + "resolved": "http://registry.npmjs.org/codemirror/-/codemirror-5.1.0.tgz", + "integrity": "sha1-7H5i7gI4QxZhqFIyUTfDP1iu5e0=" + }, + "colors": { + "version": "0.3.0", + "resolved": "http://registry.npmjs.org/colors/-/colors-0.3.0.tgz", + "integrity": "sha1-wkfWTTTbDKTcjkPz7NbamNCvlOc=" + }, + "commander": { + "version": "2.15.1", + "resolved": "http://registry.npmjs.org/commander/-/commander-2.15.1.tgz", + "integrity": "sha512-VlfT9F3V0v+jr4yxPc5gg9s62/fIVWsd2Bk2iD435um1NlGMYdVCq+MjcXnhYq2icNOizHr1kK+5TI6H0Hy0ag==", + "dev": true + }, + "concat-map": { + "version": "0.0.1", + "resolved": "https://registry.npmjs.org/concat-map/-/concat-map-0.0.1.tgz", + "integrity": "sha1-2Klr13/Wjfd5OnMDajug1UBdR3s=", + "dev": true + }, + "cover": { + "version": "0.2.9", + "resolved": "https://registry.npmjs.org/cover/-/cover-0.2.9.tgz", + "integrity": "sha1-JiAp37MXFNSAQ/7ZHt5lhZOVXdQ=", + "requires": { + "cli-table": "0.0.x", + "underscore": "1.2.x", + "underscore.string": "2.0.x", + "which": "1.0.x" + }, + "dependencies": { + "underscore": { + "version": "1.2.4", + "resolved": "http://registry.npmjs.org/underscore/-/underscore-1.2.4.tgz", + "integrity": "sha1-6NpiQaoG9k3yRzuyWQuMF8hMPH4=" + }, + "underscore.string": { + "version": "2.0.0", + "resolved": "http://registry.npmjs.org/underscore.string/-/underscore.string-2.0.0.tgz", + "integrity": "sha1-dHCFilSguzVg0DfaVtzGe1GB4Ro=" + } + } + }, + "datatables": { + "version": "1.10.6", + "resolved": "https://registry.npmjs.org/datatables/-/datatables-1.10.6.tgz", + "integrity": "sha1-JIZ6nD085hescyqneF8Sfw+109A=", + "requires": { + "jquery": ">=1.7" + } + }, + "debug": { + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/debug/-/debug-3.1.0.tgz", + "integrity": "sha512-OX8XqP7/1a9cqkxYw2yXss15f26NKWBpDXQd0/uK/KPqdQhxbPa994hnzjcE2VqQpDslf55723cKPUOGSmMY3g==", + "dev": true, + "requires": { + "ms": "2.0.0" + } + }, + "diff": { + "version": "3.5.0", + "resolved": "https://registry.npmjs.org/diff/-/diff-3.5.0.tgz", + "integrity": "sha512-A46qtFgd+g7pDZinpnwiRJtxbC1hpgf0uzP3iG89scHk0AUC7A1TGxf5OiiOUv/JMZR8GOt8hL900hV0bOy5xA==", + "dev": true + }, + "escape-string-regexp": { + "version": "1.0.5", + "resolved": "https://registry.npmjs.org/escape-string-regexp/-/escape-string-regexp-1.0.5.tgz", + "integrity": "sha1-G2HAViGQqN/2rjuyzwIAyhMLhtQ=", + "dev": true + }, + "esotope": { + "version": "1.4.5", + "resolved": "https://registry.npmjs.org/esotope/-/esotope-1.4.5.tgz", + "integrity": "sha1-oY1Tt1zwlVWZ5oMKdmFmkl3uD2k=" + }, + "estraverse": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/estraverse/-/estraverse-4.0.0.tgz", + "integrity": "sha1-q5bda+9dx5WM7B19RQhd1cjx7aE=" + }, + "fill-keys": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/fill-keys/-/fill-keys-1.0.2.tgz", + "integrity": "sha1-mo+jb06K1jTjv2tPPIiCVRRS6yA=", + "requires": { + "is-object": "~1.0.1", + "merge-descriptors": "~1.0.0" + } + }, + "fs.realpath": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz", + "integrity": "sha1-FQStJSMVjKpA20onh8sBQRmU6k8=", + "dev": true + }, + "glob": { + "version": "7.1.2", + "resolved": "https://registry.npmjs.org/glob/-/glob-7.1.2.tgz", + "integrity": "sha512-MJTUg1kjuLeQCJ+ccE4Vpa6kKVXkPYJ2mOCQyUuKLcLQsdrMCpBPUi8qVE6+YuaJkozeA9NusTAw3hLr8Xe5EQ==", + "dev": true, + "requires": { + "fs.realpath": "^1.0.0", + "inflight": "^1.0.4", + "inherits": "2", + "minimatch": "^3.0.4", + "once": "^1.3.0", + "path-is-absolute": "^1.0.0" + } + }, + "graceful-fs": { + "version": "3.0.11", + "resolved": "http://registry.npmjs.org/graceful-fs/-/graceful-fs-3.0.11.tgz", + "integrity": "sha1-dhPHeKGv6mLyXGMKCG1/Osu92Bg=", + "requires": { + "natives": "^1.1.0" + } + }, + "graceful-ncp": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/graceful-ncp/-/graceful-ncp-2.0.0.tgz", + "integrity": "sha1-3NFiko07TnK4/wR/taUkfBmxnYE=", + "requires": { + "graceful-fs": "^3.0.4", + "ncp": "^2.0.0", + "proxyquire": "^1.4.0" + } + }, + "growl": { + "version": "1.10.5", + "resolved": "https://registry.npmjs.org/growl/-/growl-1.10.5.tgz", + "integrity": "sha512-qBr4OuELkhPenW6goKVXiv47US3clb3/IbuWF9KNKEijAy9oeHxU9IgzjvJhHkUzhaj7rOUD7+YGWqUjLp5oSA==", + "dev": true + }, + "has-flag": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/has-flag/-/has-flag-3.0.0.tgz", + "integrity": "sha1-tdRU3CGZriJWmfNGfloH87lVuv0=", + "dev": true + }, + "he": { + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/he/-/he-1.1.1.tgz", + "integrity": "sha1-k0EP0hsAlzUVH4howvJx80J+I/0=", + "dev": true + }, + "inflight": { + "version": "1.0.6", + "resolved": "https://registry.npmjs.org/inflight/-/inflight-1.0.6.tgz", + "integrity": "sha1-Sb1jMdfQLQwJvJEKEHW6gWW1bfk=", + "dev": true, + "requires": { + "once": "^1.3.0", + "wrappy": "1" + } + }, + "inherits": { + "version": "2.0.3", + "resolved": "https://registry.npmjs.org/inherits/-/inherits-2.0.3.tgz", + "integrity": "sha1-Yzwsg+PaQqUC9SRmAiSA9CCCYd4=", + "dev": true + }, + "is-object": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/is-object/-/is-object-1.0.1.tgz", + "integrity": "sha1-iVJojF7C/9awPsyF52ngKQMINHA=" + }, + "jalangi2": { + "version": "github:Samsung/jalangi2#08f6f38abc2f5a09ffa48d173b7f0d92d6d8b110", + "from": "github:Samsung/jalangi2", + "requires": { + "acorn": "3.1.0", + "argparse": "0.1.6", + "codemirror": "5.1.0", + "cover": "0.2.9", + "datatables": "1.10.6", + "esotope": "1.4.5", + "estraverse": "4.0.0", + "graceful-ncp": "2.0.0", + "jquery": "2.1.3", + "mkdirp": "0.5.0", + "parse5": "2.1.5", + "q": "1.2.0", + "rewriting-proxy": "0.5.1", + "temp": "0.8.1" + }, + "dependencies": { + "mkdirp": { + "version": "0.5.0", + "resolved": "http://registry.npmjs.org/mkdirp/-/mkdirp-0.5.0.tgz", + "integrity": "sha1-HXMHam35hs2TROFecfzAWkyavxI=", + "requires": { + "minimist": "0.0.8" + } + } + } + }, + "jquery": { + "version": "2.1.3", + "resolved": "https://registry.npmjs.org/jquery/-/jquery-2.1.3.tgz", + "integrity": "sha1-bsVSBGc9UF05Qyxb9c+tEOHbrS4=" + }, + "lodash": { + "version": "4.17.11", + "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.11.tgz", + "integrity": "sha512-cQKh8igo5QUhZ7lg38DYWAxMvjSAKG0A8wGSVimP07SIUEK2UO+arSRKbRZWtelMtN5V0Hkwh5ryOto/SshYIg==" + }, + "merge-descriptors": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/merge-descriptors/-/merge-descriptors-1.0.1.tgz", + "integrity": "sha1-sAqqVW3YtEVoFQ7J0blT8/kMu2E=" + }, + "minimatch": { + "version": "3.0.4", + "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-3.0.4.tgz", + "integrity": "sha512-yJHVQEhyqPLUTgt9B83PXu6W3rx4MvvHvSUvToogpwoGDOUQ+yDrR0HRot+yOCdCO7u4hX3pWft6kWBBcqh0UA==", + "dev": true, + "requires": { + "brace-expansion": "^1.1.7" + } + }, + "minimist": { + "version": "0.0.8", + "resolved": "http://registry.npmjs.org/minimist/-/minimist-0.0.8.tgz", + "integrity": "sha1-hX/Kv8M5fSYluCKCYuhqp6ARsF0=" + }, + "mkdirp": { + "version": "0.5.1", + "resolved": "http://registry.npmjs.org/mkdirp/-/mkdirp-0.5.1.tgz", + "integrity": "sha1-MAV0OOrGz3+MR2fzhkjWaX11yQM=", + "dev": true, + "requires": { + "minimist": "0.0.8" + } + }, + "mocha": { + "version": "5.2.0", + "resolved": "https://registry.npmjs.org/mocha/-/mocha-5.2.0.tgz", + "integrity": "sha512-2IUgKDhc3J7Uug+FxMXuqIyYzH7gJjXECKe/w43IGgQHTSj3InJi+yAA7T24L9bQMRKiUEHxEX37G5JpVUGLcQ==", + "dev": true, + "requires": { + "browser-stdout": "1.3.1", + "commander": "2.15.1", + "debug": "3.1.0", + "diff": "3.5.0", + "escape-string-regexp": "1.0.5", + "glob": "7.1.2", + "growl": "1.10.5", + "he": "1.1.1", + "minimatch": "3.0.4", + "mkdirp": "0.5.1", + "supports-color": "5.4.0" + } + }, + "module-not-found-error": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/module-not-found-error/-/module-not-found-error-1.0.1.tgz", + "integrity": "sha1-z4tP9PKWQGdNbN0CsOO8UjwrvcA=" + }, + "ms": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/ms/-/ms-2.0.0.tgz", + "integrity": "sha1-VgiurfwAvmwpAd9fmGF4jeDVl8g=", + "dev": true + }, + "natives": { + "version": "1.1.6", + "resolved": "https://registry.npmjs.org/natives/-/natives-1.1.6.tgz", + "integrity": "sha512-6+TDFewD4yxY14ptjKaS63GVdtKiES1pTPyxn9Jb0rBqPMZ7VcCiooEhPNsr+mqHtMGxa/5c/HhcC4uPEUw/nA==" + }, + "ncp": { + "version": "2.0.0", + "resolved": "http://registry.npmjs.org/ncp/-/ncp-2.0.0.tgz", + "integrity": "sha1-GVoh1sRuNh0vsSgbo4uR6d9727M=" + }, + "once": { + "version": "1.4.0", + "resolved": "https://registry.npmjs.org/once/-/once-1.4.0.tgz", + "integrity": "sha1-WDsap3WWHUsROsF9nFC6753Xa9E=", + "dev": true, + "requires": { + "wrappy": "1" + } + }, + "parse5": { + "version": "2.1.5", + "resolved": "https://registry.npmjs.org/parse5/-/parse5-2.1.5.tgz", + "integrity": "sha1-eoZ3reJd2sBCN5Bfe+VGRVctzwU=" + }, + "path-is-absolute": { + "version": "1.0.1", + "resolved": "http://registry.npmjs.org/path-is-absolute/-/path-is-absolute-1.0.1.tgz", + "integrity": "sha1-F0uSaHNVNP+8es5r9TpanhtcX18=", + "dev": true + }, + "proxyquire": { + "version": "1.8.0", + "resolved": "https://registry.npmjs.org/proxyquire/-/proxyquire-1.8.0.tgz", + "integrity": "sha1-AtUUpb7ZhvBMuyCTrxZ0FTX3ntw=", + "requires": { + "fill-keys": "^1.0.2", + "module-not-found-error": "^1.0.0", + "resolve": "~1.1.7" + } + }, + "q": { + "version": "1.2.0", + "resolved": "https://registry.npmjs.org/q/-/q-1.2.0.tgz", + "integrity": "sha1-gRcFzkqYAq3/gRqw/NvQGUbh/iI=" + }, + "resolve": { + "version": "1.1.7", + "resolved": "http://registry.npmjs.org/resolve/-/resolve-1.1.7.tgz", + "integrity": "sha1-IDEU2CrSxe2ejgQRs5ModeiJ6Xs=" + }, + "rewriting-proxy": { + "version": "0.5.1", + "resolved": "https://registry.npmjs.org/rewriting-proxy/-/rewriting-proxy-0.5.1.tgz", + "integrity": "sha1-DOyH6vAtpLr2/BU+8SstyArGYh0=", + "requires": { + "parse5": "2.1.5" + } + }, + "rimraf": { + "version": "2.2.8", + "resolved": "http://registry.npmjs.org/rimraf/-/rimraf-2.2.8.tgz", + "integrity": "sha1-5Dm+Kq7jJzIZUnMPmaiSnk/FBYI=" + }, + "supports-color": { + "version": "5.4.0", + "resolved": "https://registry.npmjs.org/supports-color/-/supports-color-5.4.0.tgz", + "integrity": "sha512-zjaXglF5nnWpsq470jSv6P9DwPvgLkuapYmfDm3JWOm0vkNTVF2tI4UrN2r6jH1qM/uc/WtxYY1hYoA2dOKj5w==", + "dev": true, + "requires": { + "has-flag": "^3.0.0" + } + }, + "temp": { + "version": "0.8.1", + "resolved": "http://registry.npmjs.org/temp/-/temp-0.8.1.tgz", + "integrity": "sha1-S3tP/ehbsJ8t1rpsxDtEITyU/To=", + "requires": { + "rimraf": "~2.2.6" + } + }, + "underscore": { + "version": "1.3.3", + "resolved": "http://registry.npmjs.org/underscore/-/underscore-1.3.3.tgz", + "integrity": "sha1-R6xTaD2vgyv6lS4XdEF9pHgXrkI=" + }, + "underscore.string": { + "version": "2.1.1", + "resolved": "http://registry.npmjs.org/underscore.string/-/underscore.string-2.1.1.tgz", + "integrity": "sha1-RYOXeZEUubZ/YDC7UnsK+uaJwGE=" + }, + "which": { + "version": "1.0.9", + "resolved": "https://registry.npmjs.org/which/-/which-1.0.9.tgz", + "integrity": "sha1-RgwdoPgQED0DIam2M6+eV15kSG8=" + }, + "wrappy": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/wrappy/-/wrappy-1.0.2.tgz", + "integrity": "sha1-tSQ9jz7BqjXxNkYFvA0QNuMKtp8=", + "dev": true + } + } +} diff --git a/package.json b/package.json new file mode 100644 index 0000000..76358d3 --- /dev/null +++ b/package.json @@ -0,0 +1,37 @@ +{ + "name": "aratha", + "version": "0.0.1", + "description": "Multi-solver dynamic symbolic execution for JavaScript", + "main": "index.js", + "directories": { + "lib": "lib", + "test": "test" + }, + "scripts": { + "test": "mocha", + "analyze": "jalangi2 --analysis ." + }, + "repository": { + "type": "git", + "url": "git+https://github.com/ArathaJS/aratha.git" + }, + "keywords": [ + "dynamic symbolic execution", + "analysis" + ], + "contributors": [ + "Mak Nazecic-Andrlon ", + "Roberto Amadini " + ], + "bugs": { + "url": "https://github.com/ArathaJS/aratha/issues" + }, + "homepage": "https://github.com/ArathaJS/aratha#readme", + "devDependencies": { + "mocha": "^5.2.0" + }, + "dependencies": { + "jalangi2": "github:Samsung/jalangi2", + "lodash": "^4.17.11" + } +} diff --git a/test/testExamples.js b/test/testExamples.js index 9628637..6a0e417 100644 --- a/test/testExamples.js +++ b/test/testExamples.js @@ -11,7 +11,7 @@ const glob = require("glob"); const { testCVC4, testZ3 } = require("./testUtils"); describe("the analysis", function() { - const scriptPath = path.resolve(__dirname, "../../src/js/commands/jalangi.js"); + const scriptPath = path.resolve(__dirname, "../node_modules/jalangi2/src/js/commands/jalangi.js"); const examplesDir = path.resolve(__dirname, "examples"); const analysisDir = path.resolve(__dirname, "../"); @@ -29,7 +29,7 @@ describe("the analysis", function() { child_process.execFile( "node", [scriptPath, "--analysis", analysisDir, filePath], { env: { - SMT_SOLVER: "cvc4", + SOLVER: "cvc4", CVC4_PATH: cvc4Path } }, done); @@ -45,7 +45,7 @@ describe("the analysis", function() { child_process.execFile( "node", [scriptPath, "--analysis", analysisDir, filePath], { env: { - SMT_SOLVER: "z3", + SOLVER: "z3", Z3_PATH: z3Path } }, done);