utwente-fmt · bobismijnnaam · Jul 27, 2021 · Jul 26, 2021 · Jul 26, 2021 · Jul 26, 2021
diff --git a/.github/workflows/build-test.yml b/.github/workflows/build-test.yml
@@ -96,7 +96,7 @@ jobs:
         uses: mikepenz/action-junit-report@v2
         with:
           report_paths: '**/target/test-reports/TEST-*.xml'
-      
+
   integration-test-linux:
     needs: build-test
     runs-on: ubuntu-latest
@@ -119,7 +119,7 @@ jobs:
           name: vercors-debian-package
       - run: "sudo dpkg -i *.deb"
       - run: vercors --silicon examples/manual/fibonacci.pvl
-      - run: SPLIT=${{ matrix.testID }}/${{ env.maxTestID }} vercors --test=examples --test-workers=2 --tool carbon --tool silicon --exclude-suite=slow,medium,problem-fail --progress --actions-test-output --enable-test-coverage --coverage-output-file=jacoco_${{ matrix.testID }}_${{ env.maxTestID }}.xml
+      - run: SPLIT=${{ matrix.testID }}/${{ env.maxTestID }} vercors --test=examples --test-workers=2 --tool carbon --tool silicon --tool veymont --exclude-suite=slow,medium,problem-fail --progress --actions-test-output --enable-test-coverage --coverage-output-file=jacoco_${{ matrix.testID }}_${{ env.maxTestID }}.xml
       - name: Archive Java Code Coverage (jacoco_n_m.xml)
         uses: actions/upload-artifact@v2
         with:
@@ -186,6 +186,23 @@ jobs:
       - run: tar --strip-components=1 --directory vercorszip -xf vercors.zip
       - run: vercorszip/bin/vercors --test=examples/basic --test-workers=2 --tool carbon --tool silicon --exclude-suite=slow,medium,problem-fail --progress --actions-test-output
 
+  integration-test-veymont:
+    needs: build-test
+    runs-on: ubuntu-latest
+    steps:
+      # Need to check out the repo for the "examples" directory and the veymont 2stage testing script
+      - uses: actions/checkout@v2
+      - uses: actions/setup-java@v1
+        with:
+          java-version: "11"
+          java-package: jre
+      - name: Download VerCors binary
+        uses: actions/download-artifact@v2
+        with:
+          name: vercors-debian-package
+      - run: "sudo dpkg -i *.deb"
+      - run: ./util/veymontTesting/veymont-2stage-tests.sh
+
   sonar:
     needs:
       - build-test

diff --git a/build.sbt b/build.sbt
@@ -114,9 +114,6 @@ lazy val vercors: Project = (project in file("."))
       "-deprecation"
     ),
 
-    javacOptions += "-J-Xss128M",
-    Universal / javacOptions ++= Seq("-J-Xss128M"),
-
     buildInfoKeys := Seq[BuildInfoKey](name, version, scalaVersion, sbtVersion,
       BuildInfoKey.action("currentBranch") {
         Git.currentBranch
@@ -150,6 +147,12 @@ lazy val vercors: Project = (project in file("."))
     Compile / discoveredMainClasses := Seq(),
     Compile / mainClass := Some("vct.main.Main"),
 
+    // Add options to run scripts produced by sbt-native-packager. See: https://www.scala-sbt.org/sbt-native-packager/archetypes/java_app/customize.html#via-build-sbt
+    Universal / javaOptions ++= Seq (
+      // Needed because vercors needs a pretty big stack for some files with deep expressions.
+      "-J-Xss128m"
+    ),
+
     // Make publish-local also create a test artifact, i.e., put a jar-file into the local Ivy
     // repository that contains all classes and resources relevant for testing.
     // Other projects, e.g., Carbon or Silicon, can then depend on the Sil test artifact, which

diff --git a/examples/veymont-check/checkLTS/ltstest.pvl b/examples/veymont-check/checkLTS/ltstest.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 

diff --git a/examples/veymont-check/checkLTS/simpleifelse.pvl b/examples/veymont-check/checkLTS/simpleifelse.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 

diff --git a/examples/veymont-check/checkLTS/simplemethodcall.pvl b/examples/veymont-check/checkLTS/simplemethodcall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 

diff --git a/examples/veymont-check/checkLTS/simplewhile.pvl b/examples/veymont-check/checkLTS/simplewhile.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 

diff --git a/examples/veymont-check/checkMainClass/MainConstructorArg.pvl b/examples/veymont-check/checkMainClass/MainConstructorArg.pvl
@@ -2,6 +2,8 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
+
 class Main {
 
 

diff --git a/examples/veymont-check/checkMainClass/NoMain.pvl b/examples/veymont-check/checkMainClass/NoMain.pvl
@@ -1,6 +1,7 @@
 //:: cases NoMain
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
+//:: tool veymont
 //:: verdict Error
 class SomeClass {
 

diff --git a/examples/veymont-check/checkMainClass/NoMainConstructor.pvl b/examples/veymont-check/checkMainClass/NoMainConstructor.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 

diff --git a/examples/veymont-check/checkMainClass/NoMainMethod.pvl b/examples/veymont-check/checkMainClass/NoMainMethod.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;

diff --git a/examples/veymont-check/checkMainClass/NoMainMethod2.pvl b/examples/veymont-check/checkMainClass/NoMainMethod2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;

diff --git a/examples/veymont-check/checkMainClass/NoRunArg.pvl b/examples/veymont-check/checkMainClass/NoRunArg.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;

diff --git a/examples/veymont-check/checkMainClass/NoRunMethod.pvl b/examples/veymont-check/checkMainClass/NoRunMethod.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;

diff --git a/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl b/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 

diff --git a/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl b/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Main() {

diff --git a/examples/veymont-check/checkMainClass/WrongRunType.pvl b/examples/veymont-check/checkMainClass/WrongRunType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	int i;

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Main() {

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl
@@ -1,6 +1,7 @@
 //:: cases MainConstructorBlock
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
+//:: tool veymont
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	int i;

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	int i;

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl
@@ -1,7 +1,8 @@
 //:: cases GuardedRecursion2
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
-//:: verdict Pass
+//:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 	Role a;
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;

diff --git a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion2.pvl b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;