diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0b72c6e..8515d20 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -29,7 +29,7 @@ jobs: includePaths: 'test/include_path' timeout: 2m conditionalizePermissions: '1' - # disableNL: '1' + # disableNL: '1' - name: Verify chopped Gobra files uses: ./ with: @@ -48,6 +48,7 @@ jobs: uses: ./ with: packages: 'test/packages_test/test1/' + moreJoins: 'impure' timeout: 2m - name: Verify Gobra files (recursive mode) uses: ./ diff --git a/action.yml b/action.yml index fdf4eeb..8d67cd7 100644 --- a/action.yml +++ b/action.yml @@ -91,9 +91,9 @@ inputs: required: false default: '0' moreJoins: - description: 'Use a more complete state merging algorithm.' + description: 'Specifies if silicon should be run with more joins completely enabled ("all"), disabled ("off"), or only for impure conditionals ("impure").' required: false - default: '0' + default: 'off' unsafeWildcardOptimization: description: "Perform the optimization described in silicon's PR #756. You must ensure that the necessary conditions for the optimization are met." required: false diff --git a/docker-action/entrypoint.sh b/docker-action/entrypoint.sh index cee8368..7540df2 100644 --- a/docker-action/entrypoint.sh +++ b/docker-action/entrypoint.sh @@ -129,9 +129,7 @@ if [[ $INPUT_CONDITIONALIZEPERMISSIONS -eq 1 ]]; then GOBRA_ARGS="$GOBRA_ARGS --conditionalizePermissions" fi -if [[ $INPUT_MOREJOINS -eq 1 ]]; then - GOBRA_ARGS="$GOBRA_ARGS --moreJoins" -fi +GOBRA_ARGS="$GOBRA_ARGS --moreJoins $INPUT_MOREJOINS" if [[ $INPUT_OVERFLOW -eq 1 ]]; then GOBRA_ARGS="$GOBRA_ARGS --overflow"