From 77b5e1e2de28498d8caea7d028a06d1c6df89abe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Thu, 23 Jun 2022 13:29:10 +0200
Subject: [PATCH 1/3] Add checkConsistency flag to CI

---
 .github/workflows/test.yml  | 3 ++-
 action.yml                  | 4 ++++
 docker-action/entrypoint.sh | 7 ++++++-
 entrypoint.sh               | 2 +-
 4 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index dc585f3..a1001d0 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -34,6 +34,7 @@ jobs:
           excludePackages: 'main'
           recursive: '1'
           packageTimeout: 2m
+          checkConsistency: '1'
       - name: Verify Gobra files (recursive and headerOnly mode)
         uses: ./
         with:
@@ -41,4 +42,4 @@ jobs:
           excludePackages: 'main'
           recursive: '1'
           headerOnly: '1'
-          packageTimeout: 2m
\ No newline at end of file
+          packageTimeout: 2m
diff --git a/action.yml b/action.yml
index b6b3335..5368321 100644
--- a/action.yml
+++ b/action.yml
@@ -65,6 +65,10 @@ inputs:
     description: 'Assume injectivity of the receiver expression when inhaling quantified permissions, instead of checking it, like in Viper versions previous to 2022.02.'
     required: false
     default: '1'
+  checkConsistency:
+    decription: 'Enforces additional consistency checks in the generated Viper code. Helpful to debug problems with the encoding of Gobra.'
+    required: false
+    default: '0'
 outputs:
   time:
     description: 'Total verification time in seconds'
diff --git a/docker-action/entrypoint.sh b/docker-action/entrypoint.sh
index c25aaf9..6a8381a 100644
--- a/docker-action/entrypoint.sh
+++ b/docker-action/entrypoint.sh
@@ -95,6 +95,11 @@ else
     GOBRA_ARGS="$GOBRA_ARGS --noassumeInjectivityOnInhale"
 fi
 
+if [[ $INPUT_CHECKCONSISTENCY -eq 1 ]]; then
+    GOBRA_ARGS="$GOBRA_ARGS --checkConsistency"
+fi
+
+
 START_TIME=$SECONDS
 EXIT_CODE=0
 
@@ -117,4 +122,4 @@ TIME_PASSED=$[ $SECONDS-$START_TIME ]
 
 echo "::set-output name=time::$TIME_PASSED"
 
-exit $EXIT_CODE
\ No newline at end of file
+exit $EXIT_CODE
diff --git a/entrypoint.sh b/entrypoint.sh
index c0007b5..71b7557 100644
--- a/entrypoint.sh
+++ b/entrypoint.sh
@@ -4,7 +4,7 @@ echo "Creating a docker image with Gobra image tag: $INPUT_IMAGEVERSION"
 docker build -t docker-action --build-arg "image_version=$INPUT_IMAGEVERSION" --build-arg "image_name=$INPUT_IMAGENAME" /docker-action
 
 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_GLOBALTIMEOUT -e INPUT_PACKAGETIMEOUT -e INPUT_HEADERONLY -e INPUT_MODULE -e INPUT_RECURSIVE -e INPUT_ASSUMEINJECTIVITYONINHALE -e GITHUB_WORKSPACE -e GITHUB_REPOSITORY \
+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_GLOBALTIMEOUT -e INPUT_PACKAGETIMEOUT -e INPUT_HEADERONLY -e INPUT_MODULE -e INPUT_RECURSIVE -e INPUT_ASSUMEINJECTIVITYONINHALE -e INPUT_CHECKCONSISTENCY -e GITHUB_WORKSPACE -e GITHUB_REPOSITORY \
   -v $RUNNER_WORKSPACE:$GITHUB_WORKSPACE \
   --workdir $GITHUB_WORKSPACE docker-action
 

From 60f3e0389f546358c7a1c4f1560f17cc8b953543 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Thu, 23 Jun 2022 13:42:41 +0200
Subject: [PATCH 2/3] Incorporate feedback from ShellCheck

---
 docker-action/entrypoint.sh | 16 ++++++++--------
 entrypoint.sh               |  4 ++--
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/docker-action/entrypoint.sh b/docker-action/entrypoint.sh
index 6a8381a..8a09978 100644
--- a/docker-action/entrypoint.sh
+++ b/docker-action/entrypoint.sh
@@ -21,11 +21,11 @@ REPOSITORY_NAME=$(echo "$GITHUB_REPOSITORY" | awk -F / '{print $2}' | sed -e "s/
 # absolute path. Note: does not handle paths that contain a space.
 getFileListInDir () (
     local LOCATION=$1
-    cd -- "$LOCATION"
+    cd -- "$LOCATION" || exit
     # the tail of the list of arguments (i.e., the args without
     # the function name and the first argument (LOCATION) are
     # the list of paths to be processed.
-    echo "$(echo "${@:2}" | xargs realpath | tr '\n' ' ')"
+    "$(echo "${@:2}" | xargs realpath | tr '\n' ' ')"
 )
 
 GOBRA_JAR="/gobra/gobra.jar"
@@ -43,7 +43,7 @@ if [[ $INPUT_RECURSIVE -eq 1 ]]; then
 fi
 
 if [[ $INPUT_FILES ]]; then
-    RESOLVED_PATHS="$(getFileListInDir $PROJECT_LOCATION $INPUT_FILES)"
+    RESOLVED_PATHS="$(getFileListInDir "$PROJECT_LOCATION" "$INPUT_FILES")"
     echo "[DEBUG] Project Location: $PROJECT_LOCATION" > $DEBUG_OUT
     echo "[DEBUG] Input Files: $INPUT_FILES" > $DEBUG_OUT
     echo "[DEBUG] Resolved Paths: $RESOLVED_PATHS" > $DEBUG_OUT
@@ -52,12 +52,12 @@ fi
 
 if [[ $INPUT_PACKAGES ]]; then
     # INPUT_PACKAGES are paths to packages
-    RESOLVED_PATHS="$(getFileListInDir $PROJECT_LOCATION $INPUT_PACKAGES)"
+    RESOLVED_PATHS="$(getFileListInDir "$PROJECT_LOCATION" "$INPUT_PACKAGES")"
     GOBRA_ARGS="-p $RESOLVED_PATHS $GOBRA_ARGS"
 fi
 
 if [[ $INPUT_INCLUDEPATHS ]]; then
-    RESOLVED_PATHS=$(getFileListInDir $PROJECT_LOCATION $INPUT_INCLUDEPATHS)
+    RESOLVED_PATHS=$(getFileListInDir "$PROJECT_LOCATION" "$INPUT_INCLUDEPATHS")
     echo "[DEBUG] Project Location: $PROJECT_LOCATION" > $DEBUG_OUT
     echo "[DEBUG] Include Paths: $INPUT_INCLUDEPATHS" > $DEBUG_OUT
     echo "[DEBUG] Resolved Paths: $RESOLVED_PATHS" > $DEBUG_OUT
@@ -105,9 +105,9 @@ EXIT_CODE=0
 
 CMD="java $JAVA_ARGS $GOBRA_ARGS"
 
-echo $CMD
+echo "$CMD"
 
-if timeout $INPUT_GLOBALTIMEOUT $CMD; then
+if timeout "$INPUT_GLOBALTIMEOUT" "$CMD"; then
     echo -e "${GREEN}Verification completed successfully${RESET}"
 else
     EXIT_CODE=$?
@@ -118,7 +118,7 @@ else
     fi
 fi
 
-TIME_PASSED=$[ $SECONDS-$START_TIME ]
+TIME_PASSED=$((SECONDS-START_TIME))
 
 echo "::set-output name=time::$TIME_PASSED"
 
diff --git a/entrypoint.sh b/entrypoint.sh
index 71b7557..78ac5d7 100644
--- a/entrypoint.sh
+++ b/entrypoint.sh
@@ -5,6 +5,6 @@ docker build -t docker-action --build-arg "image_version=$INPUT_IMAGEVERSION" --
 
 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_GLOBALTIMEOUT -e INPUT_PACKAGETIMEOUT -e INPUT_HEADERONLY -e INPUT_MODULE -e INPUT_RECURSIVE -e INPUT_ASSUMEINJECTIVITYONINHALE -e INPUT_CHECKCONSISTENCY -e GITHUB_WORKSPACE -e GITHUB_REPOSITORY \
-  -v $RUNNER_WORKSPACE:$GITHUB_WORKSPACE \
-  --workdir $GITHUB_WORKSPACE docker-action
+  -v "$RUNNER_WORKSPACE:$GITHUB_WORKSPACE" \
+  --workdir "$GITHUB_WORKSPACE" docker-action
 

From c57aa3ee879d7b6ff9252de414ea81c88dc06e77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Thu, 23 Jun 2022 13:45:40 +0200
Subject: [PATCH 3/3] Test change

---
 docker-action/entrypoint.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docker-action/entrypoint.sh b/docker-action/entrypoint.sh
index 8a09978..be89236 100644
--- a/docker-action/entrypoint.sh
+++ b/docker-action/entrypoint.sh
@@ -25,7 +25,7 @@ getFileListInDir () (
     # the tail of the list of arguments (i.e., the args without
     # the function name and the first argument (LOCATION) are
     # the list of paths to be processed.
-    "$(echo "${@:2}" | xargs realpath | tr '\n' ' ')"
+    echo "$(echo "${@:2}" | xargs realpath | tr '\n' ' ')"
 )
 
 GOBRA_JAR="/gobra/gobra.jar"