More gobra flags (#16)

* test * add test Co-authored-by: João Pereira <[email protected]>
viperproject · Nov 18, 2022 · 20ad0ad · 20ad0ad
1 parent ebb3962
commit 20ad0ad
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 2 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -50,6 +50,13 @@ jobs:
           headerOnly: '1'
           timeout: 2m
           statsFile: '/stats/'
+      - name: Verify Gobra files (disableMoreCompleteExhale and parallelizeBranches)
+        uses: ./
+        with:
+          packages: 'test/packages_test/test1/'
+          timeout: 2m
+          disableMoreCompleteExhale: 1
+          parallelizeBranches: 1
       - name: Test that timeout reports an error
         continue-on-error: true
         uses: ./

diff --git a/action.yml b/action.yml
@@ -66,6 +66,14 @@ inputs:
     decription: 'Enforces additional consistency checks in the generated Viper code. Helpful to debug problems with the encoding of Gobra.'
     required: false
     default: '0'
+  disableMoreCompleteExhale:
+    description: 'Disables more complete exhale.'
+    required: false
+    default: '0'
+  parallelizeBranches:
+    description: 'Parallelize branches in the silicon backend.'
+    required: false
+    default: '0'
   statsFile:
     description: 'Path where the generated stats.json file will be stored'
     required: false

diff --git a/docker-action/entrypoint.sh b/docker-action/entrypoint.sh
@@ -101,6 +101,14 @@ if [[ $INPUT_CHECKCONSISTENCY -eq 1 ]]; then
 	GOBRA_ARGS="$GOBRA_ARGS --checkConsistency"
 fi
 
+if [[ $INPUT_DISABLEMORECOMPLETEEXHALE -eq 1 ]]; then
+	GOBRA_ARGS="$GOBRA_ARGS --disableMoreCompleteExhale"
+fi
+
+if [[ $INPUT_PARALLELIZEBRANCHES -eq 1 ]]; then
+	GOBRA_ARGS="$GOBRA_ARGS --parallelizeBranches"
+fi
+
 if [[ $INPUT_STATSFILE ]]; then
 	# We write the file to /tmp/ (which is easier then making gobra write directly
 	# to the STATS_TARGET, as doing so often causes Gobra to not generate a file) due

diff --git a/entrypoint.sh b/entrypoint.sh
@@ -9,6 +9,7 @@ export STATS_TARGET="/stats/"
 echo "Run Docker Action container"
 docker run -e INPUT_CACHING -e INPUT_PROJECTLOCATION -e INPUT_INCLUDEPATHS -e INPUT_FILES -e INPUT_PACKAGES -e INPUT_EXCLUDEPACKAGES -e INPUT_CHOP \
   -e INPUT_VIPERBACKEND -e INPUT_JAVAXSS -e INPUT_JAVAXMX -e INPUT_TIMEOUT -e INPUT_HEADERONLY -e INPUT_STATSFILE \
-  -e INPUT_MODULE -e INPUT_RECURSIVE -e INPUT_ASSUMEINJECTIVITYONINHALE -e INPUT_CHECKCONSISTENCY -e GITHUB_WORKSPACE -e GITHUB_REPOSITORY \
+  -e INPUT_MODULE -e INPUT_RECURSIVE -e INPUT_ASSUMEINJECTIVITYONINHALE -e INPUT_CHECKCONSISTENCY -e INPUT_DISABLEMORECOMPLETEEXHALE \
+  -e INPUT_PARALLELIZEBRANCHES -e GITHUB_WORKSPACE -e GITHUB_REPOSITORY \
   -e STATS_TARGET -e DEBUG_MODE -v "$RUNNER_WORKSPACE:$GITHUB_WORKSPACE" -v "$INPUT_STATSFILE:$STATS_TARGET" \
-  --workdir "$GITHUB_WORKSPACE" docker-action
+  --workdir "$GITHUB_WORKSPACE" docker-action