replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Print command line nicely in script 

This allow to have a command line that can directly be executed when
extracted from the json output.
This commit is contained in:
Romain Brenguier 2019-03-18 09:40:20 +00:00
parent 0db1830c6d
commit 487f594123
1 changed files with 10 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
scripts/benchmark/benchmark_java_project.js
View File

@ -50,6 +50,14 @@ function argsToArray(args) {
return result;
}
function arrayToString(args) {
let result = "";
for(let i = 0; i < args.length; i++) {
result = result + args[i] + " ";
}
return result
}
/// Get the coverage info from the json output if available
function readCoverageInfo(stdout) {
const jsonOutput = JSON.parse(stdout);
@ -104,7 +112,7 @@ function run(executable, modelsPath, argumentsFile, functionName,
let result = {
classFile: classFile, function: functionName,
execTime: execTime, success: true,
commandLine: command
commandLine: arrayToString(command)
}
if (showProperties) {
result.goals = readNumberOfGoals(output);
@ -116,7 +124,7 @@ function run(executable, modelsPath, argumentsFile, functionName,
return JSON.stringify({
classFile: classFile, function: functionName,
execTime: (new Date() - startTime) / 1000, success: false,
commandLine: command
commandLine: arrayToString(command)
});
}
}