Merge pull request #469 from viperproject/gobra-issue-823

Enables plugins within ViperServer

client/src/test/data/decreases.gobra

@@ -0,0 +1,12 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package decrease
+
+// this test case checks that Gobra / GobraServer correctly invokes
+// Viper plugins as verifying this file requires the termination plugin.
+
+decreases i
+func infiniteRecursion(i int) {
+    infiniteRecursion(i - 1)
+}

client/src/test/extension.test.ts

@@ -21,6 +21,7 @@ const ASSERT_TRUE = "assert_true.gobra";
 const ASSERT_FALSE = "assert_false.gobra";
 const FAILING_POST_GOBRA = "failing_post.gobra";
 const FAILING_POST_GO = "failing_post.go";
+const DECREASES = "decreases.gobra";
 const PKG_FILE_1 = "pkg/file1.gobra";
 
 const URL_CONVERSION_TIMEOUT_MS = 5000; // 5s
@@ -230,6 +231,20 @@ suite("Extension", () => {
         );
     });
 
+    test("Verify program requiring Viper plugins and underline non-terminating recursive call (Gobra Issue #823)", async function() {
+        this.timeout(GOBRA_VERIFICATION_TIMEOUT_MS);
+        const document = await openAndVerifyFile(DECREASES);
+        const diagnostics = vscode.languages.getDiagnostics(document.uri);
+        assert.ok(
+            diagnostics.some(
+                (diagnostic) => (
+                    document.getText(diagnostic.range).includes("infiniteRecursion(i - 1)")
+                )
+            ),
+            "The non-terminating recursive call was not reported."
+        );
+    });
+
     test("Verifying basic programs as a package fails because of differing package names", async function() {
         this.timeout(GOBRA_VERIFICATION_TIMEOUT_MS);
         // note: we have to consider the diagnostics of all gobra and go files because we do not want

server/src/main/scala/viper/gobraserver/GobraServerService.scala

@@ -24,7 +24,7 @@ class GobraServerService(config: ServerConfig)(implicit executor: GobraServerExe
     // always send full text document for each notification:
     capabilities.setTextDocumentSync(TextDocumentSyncKind.Incremental)
 
-    val options: List[String] = List("--disablePlugins", "--logLevel", config.logLevel.levelStr)
+    val options: List[String] = List("--logLevel", config.logLevel.levelStr)
     GobraServer.init(options)(executor)
     GobraServer.start()