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..be89236 100644 --- a/docker-action/entrypoint.sh +++ b/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 \ No newline at end of file +exit $EXIT_CODE diff --git a/entrypoint.sh b/entrypoint.sh index c0007b5..78ac5d7 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 \ - -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