Add option disableNL

.github/workflows/test.yml

@@ -29,6 +29,7 @@ jobs:
           includePaths: 'test/include_path'
           timeout: 2m
           conditionalizePermissions: '1'
+          disableNL: '1'
       - name: Verify chopped Gobra files
         uses: ./
         with:

action.yml

@@ -86,6 +86,10 @@ inputs:
     description: 'Tries to reduce the number of branches that Gobra has to deal with the option --conditionalizePermissions'
     required: false
     default: '0'
+  disableNL:
+    description: 'Disable non-linear integer arithmetic. Non compatible yet with Carbon'
+    required: false
+    default: '0'
   useZ3API:
     description: 'Use the Z3 API in silicon.'
     required: false

docker-action/entrypoint.sh

@@ -117,6 +117,11 @@ if [[ $INPUT_REQUIRETRIGGERS -eq 1 ]]; then
 	GOBRA_ARGS="$GOBRA_ARGS --requireTriggers"
 fi
 
+if [[ $INPUT_DISABLENL -eq 1 ]]; then
+	GOBRA_ARGS="$GOBRA_ARGS --disableNL"
+fi
+
+
 if [[ $INPUT_CONDITIONALIZEPERMISSIONS -eq 1 ]]; then
 	GOBRA_ARGS="$GOBRA_ARGS --conditionalizePermissions"
 fi

entrypoint.sh

@@ -11,7 +11,7 @@ docker run -e INPUT_CACHING -e INPUT_PROJECTLOCATION -e INPUT_INCLUDEPATHS -e IN
  -e INPUT_OVERFLOW  -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 INPUT_MCEMODE \
   -e INPUT_REQUIRETRIGGERS \
-  -e INPUT_USEZ3API \
+  -e INPUT_USEZ3API -e INPUT_DISABLENL \
   -e INPUT_PARALLELIZEBRANCHES -e INPUT_CONDITIONALIZEPERMISSIONS -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