Removes redundant re-running of kani process

package.json

@@ -7,7 +7,7 @@
     "type": "git",
     "url": "https://github.com/model-checking/kani-vscode-extension"
   },
-  "version": "0.0.2",
+  "version": "0.0.4",
   "engines": {
     "vscode": "^1.70.0"
   },

src/model/kaniCommandCreate.ts

@@ -21,7 +21,18 @@ export async function runKaniHarnessInterface(harnessName: string, args?: number
 		harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.harnessFlag} ${harnessName} ${KaniArguments.unwindFlag} ${args}`;
 	}
 	const kaniOutput = await catchOutput(harnessCommand);
-	return kaniOutput;
+	if (typeof kaniOutput == 'number') {
+		return [kaniOutput, ''];
+	} else if (
+		Array.isArray(kaniOutput) &&
+		kaniOutput.length == 2 &&
+		typeof kaniOutput[0] === 'number' &&
+		typeof kaniOutput[1] === 'object'
+	) {
+		return kaniOutput;
+	} else {
+		return [5, ''];
+	}
 }
 
 /**
@@ -97,7 +108,7 @@ export async function runCommandPure(command: string): Promise<void> {
 }
 
 // Run a command and capture the command line output into a string
-async function catchOutput(command: string, cargoKaniMode: boolean = false): Promise<number> {
+async function catchOutput(command: string, cargoKaniMode: boolean = false): Promise<any> {
 	const process = await runKaniCommand(command);
 	return process;
 }

src/model/kaniRunner.ts

@@ -150,7 +150,12 @@ function executeKaniProcess(
 			} else if (error) {
 				if (error.code === 1) {
 					// verification failed
-					resolve(1);
+					if (stdout) {
+						const responseObject: KaniResponse = responseParserInterface(stdout.toString('utf-8'));
+						resolve([1, responseObject]);
+					} else {
+						resolve(1);
+					}
 				} else {
 					// Error is an object created by nodejs created when nodejs cannot execute the command
 					vscode.window.showErrorMessage(

src/test-tree/createTests.ts

@@ -212,20 +212,25 @@ export class TestCase {
 	async run(item: vscode.TestItem, options: vscode.TestRun): Promise<void> {
 		const start: number = Date.now();
 		if (this.proof_boolean) {
-			const actual: number = await this.evaluate(
+			const actualResult: any = await this.evaluate(
 				this.file_name,
 				this.harness_name,
 				this.harness_unwind_value,
 			);
+
+			const actual = actualResult[0];
+
 			const duration: number = Date.now() - start;
 			if (actual === 0) {
 				options.passed(item, duration);
 			} else {
+				const responseObject: KaniResponse | string = actualResult[1];
+
+				if (typeof responseObject == 'string') {
+					return;
+				}
+
 				const location = new vscode.Location(item.uri!, item.range!);
-				const responseObject: KaniResponse = await captureFailedChecks(
-					this.harness_name,
-					this.harness_unwind_value,
-				);
 				const failedChecks: string = responseObject.failedProperty;
 				const failedMessage: string = responseObject.failedMessages;
 				const currentCase = new FailedCase(
@@ -270,18 +275,22 @@ export class TestCase {
 	}
 
 	// Run kani on the file, crate with given arguments
-	async evaluate(rsFile: string, harness_name: string, args?: number): Promise<number> {
+	async evaluate(
+		rsFile: string,
+		harness_name: string,
+		args?: number,
+	): Promise<[number, KaniResponse | string]> {
 		if (vscode.workspace.workspaceFolders !== undefined) {
 			if (args === undefined || NaN) {
-				const outputKani: number = await runKaniHarnessInterface(harness_name);
+				const outputKani: any = await runKaniHarnessInterface(harness_name);
 				return outputKani;
 			} else {
-				const outputKani: number = await runKaniHarnessInterface(harness_name, args);
+				const outputKani: any = await runKaniHarnessInterface(harness_name, args);
 				return outputKani;
 			}
 		}
 
-		return 0;
+		return [0, ''];
 	}
 
 	// Run kani on bolero test case, file, crate with given arguments