New features and improvements

recompile.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+npm run compile
+
+code --extensionDevelopmentPath=/home/juppi/prgs/prusti-assistant /home/juppi/docs/ETH/HS22/PrustiAssistant/examples/ --disable-extensions
+

snippets/specs.json

@@ -19,5 +19,26 @@
             "body_invariant!(${1:true});"
         ],
         "description": "Insert body_invariant!(...);"
+    },
+    "pure": {
+        "prefix": "pure",
+        "body": [
+            "#[pure]"
+        ],
+        "description": "Insert #[pure]"
+    },
+    "trusted": {
+        "prefix": "trusted",
+        "body": [
+            "#[trusted]"
+        ],
+        "description": "Insert #[trusted]"
+    },
+    "externSpec": {
+        "prefix": "extern_spec",
+        "body": [
+            "#[extern_spec($1)]"
+        ],
+        "description": "Insert #[extern_spec(...)]"
     }
 }

src/config.ts

@@ -100,3 +100,11 @@ export function extraCargoPrustiArgs(): string[] {
 export function extraPrustiServerArgs(): string[] {
     return config().get("extraPrustiServerArgs", []);
 }
+
+export function contractsAsDefinitions(): boolean {
+    return config().get("contractsAsDefinitions", false);
+}
+
+export function reportViperMessages(): boolean {
+    return config().get("reportViperMessages", true);
+}

src/dependencies/index.ts

@@ -9,6 +9,7 @@ import { PrustiLocation } from "./PrustiLocation";
 import { prustiTools } from "./prustiTools";
 
 export let prusti: PrustiLocation | undefined;
+export let prustiSemanticVersion: string = "0.0.0";
 export async function installDependencies(context: vscode.ExtensionContext, shouldUpdate: boolean, verificationStatus: vscode.StatusBarItem): Promise<void> {
     try {
         util.log(`${shouldUpdate ? "Updating" : "Installing"} Prusti dependencies...`);
@@ -49,12 +50,10 @@ export async function installDependencies(context: vscode.ExtensionContext, shou
             prusti.rustToolchainFile(),
         );
     } catch (err) {
-        util.userError(
-            `Error installing Prusti. Please restart the IDE to retry. Details: ${err}`,
-            true, verificationStatus
-        );
+        util.userError(`Error installing Prusti: ${err}`, true, verificationStatus);
         throw err;
     } finally {
+        await updatePrustiSemVersion();
         await server.restart(context, verificationStatus);
     }
 }
@@ -72,3 +71,12 @@ export async function prustiVersion(): Promise<string> {
     }
     return version;
 }
+
+export async function updatePrustiSemVersion() {
+    let version = await prustiVersion();
+    // version will have the form Prusti version: 0.x.x, commit 234..hash..
+    let result = version.split(" ")[2].slice(0, -1);
+    util.log("Setting prustiVersion to " + result);
+    prustiSemanticVersion = result;
+}
+