Merge branch 'master' into viper-release

.github/license-check/config.json

@@ -5,7 +5,8 @@
       "**/*.vpr",
       "**/*.go",
       "build.sbt",
-      "src/main/resources/stubs/github.com/**/*.gobra"
+      "src/main/resources/stubs/github.com/**/*.gobra",
+      "**/Gobra*.g4"
     ],
     "exclude": [
       "carbon/**",
@@ -15,7 +16,8 @@
       "project/project/**",
       "project/target/**",
       "target/**",
-      "src/test/resources/**/*.go"
+      "src/test/resources/**/*.go",
+      "src/test/scala/viper/gobra/parsing/GoParserUnitTests.scala"
     ],
     "license": "./.github/license-check/headers/MPLv2-ETH.txt"
   },
@@ -89,16 +91,27 @@
       "docs/**",
       "artifact/content/paper.pdf",
       "artifact/content/tutorial.md",
-      "artifact/evaluation/**"
+      "artifact/evaluation/**",
+      "src/main/java/**/*.java"
     ]
   },
   {
     "include": [
-      "src/main/**/*.gobra"
+      "src/main/**/*.gobra",
+      "src/test/scala/viper/gobra/parsing/GoParserUnitTests.scala"
     ],
     "exclude": [
       "src/main/resources/stubs/github.com/**/*.gobra"
     ],
     "license": "./.github/license-check/headers/Go.txt"
+  },
+  {
+    "include": [
+      "src/main/**/*.g4"
+    ],
+    "exclude": [
+      "src/main/**/Gobra*.g4"
+    ],
+    "license": "./.github/license-check/headers/BSD-3-SIDM.txt"
   }
 ]

.github/license-check/headers/BSD-3-SIDM.txt

@@ -0,0 +1,30 @@
+/*
+ [The "BSD licence"]
+ Copyright (c) 2017 Sasa Coh, Michał Błotniak
+ Copyright (c) 2019 Ivan Kochurkin, [email protected], Positive Technologies
+ Copyright (c) 2019 Dmitry Rassadin, [email protected], Positive Technologies
+ Copyright (c) 2021 Martin Mirchev, [email protected]
+ All rights reserved.
+
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions
+ are met:
+ 1. Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+ 2. Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in the
+    documentation and/or other materials provided with the distribution.
+ 3. The name of the author may not be used to endorse or promote products
+    derived from this software without specific prior written permission.
+
+ THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
+ IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
+ OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
+ IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
+ INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
+ NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
+ THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/

.gitignore

@@ -14,6 +14,12 @@ logger.log
 
 *.go.*
 *.gobra.*
+/src/main/java/viper/gobra/frontend/GobraLexer.tokens
+/src/main/java/viper/gobra/frontend/GobraParser.interp
+/src/main/java/viper/gobra/frontend/GobraParser.tokens
+/gen/
+/.gobra/
+
 .bloop/
 .metals/
 .vscode/

build.sbt

@@ -42,13 +42,14 @@ lazy val gobra = (project in file("."))
     libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.9", // for SystemUtils
     libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
     libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
+    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.9.2",
 
     scalacOptions ++= Seq(
       "-encoding", "UTF-8", // Enforce UTF-8, instead of relying on properly set locales
       "-Ypatmat-exhaust-depth", "40"
     ),
 
-    javacOptions ++= Seq("-encoding", "UTF-8", "-charset", "UTF-8", "-docencoding", "UTF-8"),
+    javacOptions := Seq("-encoding", "UTF-8"),
 
     // Run settings
     run / javaOptions ++= Seq(
@@ -57,6 +58,7 @@ lazy val gobra = (project in file("."))
     ),
 
     fork := true,
+    cancelable in Global := true,
 
 
     // Test settings