Clean up

src/crateMetadata.ts

@@ -2,23 +2,13 @@ import * as util from "./util";
 import * as config from "./config";
 import * as dependencies from "./dependencies";
 
-interface CargoMetadata {
+export interface CrateMetadata {
     target_directory: string;
     workspace_root?: string;
 }
 
-/**
- * Parses the output of `cargo metadata` into a `CargoMetadata` object.
- *
- * @param output The output to parse.
- */
-function parseCargoMetadata(output: string): CargoMetadata {
-    return JSON.parse(output) as CargoMetadata;
-}
-
-export enum MetadataStatus {
-    Crash,
-    Errors,
+export enum CrateMetadataStatus {
+    Error,
     Ok
 }
 
@@ -30,7 +20,11 @@ export enum MetadataStatus {
  * @param destructors Where to store the destructors of the spawned processes.
  * @returns A tuple containing the metadata, the exist status, and the duration of the query.
  */
-export async function queryCrateMetadata(prusti: dependencies.PrustiLocation, cratePath: string, destructors: Set<util.KillFunction>): Promise<[CargoMetadata, MetadataStatus, util.Duration]> {
+export async function queryCrateMetadata(
+    prusti: dependencies.PrustiLocation,
+    cratePath: string,
+    destructors: Set<util.KillFunction>,
+): Promise<[CrateMetadata, CrateMetadataStatus, util.Duration]> {
     const cargoPrustiArgs = ["--no-deps", "--offline", "--format-version=1"].concat(
         config.extraCargoPrustiArgs()
     );
@@ -53,22 +47,16 @@ export async function queryCrateMetadata(prusti: dependencies.PrustiLocation, cr
         },
         destructors,
     );
-    let status = MetadataStatus.Crash;
+    let status = CrateMetadataStatus.Error;
     if (output.code === 0) {
-        status = MetadataStatus.Ok;
-    }
-    if (output.code === 1) {
-        status = MetadataStatus.Errors;
-    }
-    if (output.code === 101) {
-        status = MetadataStatus.Errors;
+        status = CrateMetadataStatus.Ok;
     }
     if (/error: internal compiler error/.exec(output.stderr) !== null) {
-        status = MetadataStatus.Crash;
+        status = CrateMetadataStatus.Error;
     }
     if (/^thread '.*' panicked at/.exec(output.stderr) !== null) {
-        status = MetadataStatus.Crash;
+        status = CrateMetadataStatus.Error;
     }
-    const metadata: CargoMetadata = parseCargoMetadata(output.stdout);
+    const metadata = JSON.parse(output.stdout) as CrateMetadata;
     return [metadata, status, output.duration];
 }

src/diagnostics.ts

@@ -4,7 +4,7 @@ import * as vscode from "vscode";
 import * as path from "path";
 import * as vvt from "vs-verification-toolbox";
 import * as dependencies from "./dependencies";
-import { queryCrateMetadata, MetadataStatus } from "./crateMetadata";
+import { queryCrateMetadata, CrateMetadataStatus } from "./crateMetadata";
 
 // ========================================================
 // JSON Schemas
@@ -350,11 +350,16 @@ enum VerificationStatus {
  * @param prusti The location of Prusti files.
  * @param cratePath The path of a Rust crate.
  * @param destructors Where to store the destructors of the spawned processes.
- * @returns A tuple containing the metadata, the exist status, and the duration of the query.
+ * @returns A tuple containing the diagnostics, status and duration of the verification.
  */
-async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, cratePath: string, serverAddress: string, destructors: Set<util.KillFunction>): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
+async function queryCrateDiagnostics(
+    prusti: dependencies.PrustiLocation,
+    cratePath: string,
+    serverAddress: string,
+    destructors: Set<util.KillFunction>,
+): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
     const [metadata, metadataStatus, metadataDuration] = await queryCrateMetadata(prusti, cratePath, destructors);
-    if (metadataStatus !== MetadataStatus.Ok) {
+    if (metadataStatus !== CrateMetadataStatus.Ok) {
         return [[], VerificationStatus.Crash, metadataDuration];
     }
 
@@ -411,12 +416,19 @@ async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, crateP
 }
 
 /**
- * Queries for the diagnostics of a rust program using prusti-rustc.
+ * Queries for the diagnostics of a rust crate using prusti-rustc.
  *
- * @param filePath The path of the file on which to run prusti-rustc.
- * @returns An array of diagnostics for the given rust project.
+ * @param prusti The location of Prusti files.
+ * @param filePath The path of a Rust program.
+ * @param destructors Where to store the destructors of the spawned processes.
+ * @returns A tuple containing the diagnostics, status and duration of the verification.
  */
-async function queryProgramDiagnostics(prusti: dependencies.PrustiLocation, filePath: string, serverAddress: string, destructors: Set<util.KillFunction>): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
+async function queryProgramDiagnostics(
+    prusti: dependencies.PrustiLocation,
+    filePath: string,
+    serverAddress: string,
+    destructors: Set<util.KillFunction>,
+): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
     const prustiRustcArgs = [
         "--crate-type=lib",
         "--error-format=json",