Shellcheck

.github/workflows/test.yml

@@ -34,11 +34,12 @@ jobs:
           excludePackages: 'main'
           recursive: '1'
           packageTimeout: 2m
+          checkConsistency: '1'
       - name: Verify Gobra files (recursive and headerOnly mode)
         uses: ./
         with:
           projectLocation: 'gobra-action/test/'
           excludePackages: 'main'
           recursive: '1'
           headerOnly: '1'
-          packageTimeout: 2m
+          packageTimeout: 2m

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'

docker-action/entrypoint.sh

@@ -21,7 +21,7 @@ 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.
@@ -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
@@ -95,14 +95,19 @@ 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
 
 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=$?
@@ -113,8 +118,8 @@ else
     fi
 fi
 
-TIME_PASSED=$[ $SECONDS-$START_TIME ]
+TIME_PASSED=$((SECONDS-START_TIME))
 
 echo "::set-output name=time::$TIME_PASSED"
 
-exit $EXIT_CODE
+exit $EXIT_CODE

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 \
-  -v $RUNNER_WORKSPACE:$GITHUB_WORKSPACE \
-  --workdir $GITHUB_WORKSPACE docker-action
+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