Add support for checking for overflows (#22)

* add overflow flag

* fix termination checking

action.yml

@@ -24,6 +24,10 @@ inputs:
     description: 'Verify nested packages recursively'
     required: false
     default:  '0'
+  overflow:
+    description: 'Check for arithmetic overflows in integer expressions.'
+    required: false
+    default:  '0'
   chop:
     description: 'Maximum number of files in which a file can be split with the chopper feature of Gobra. Larger values may improve the verification time of large codebases.'
     default: '1'

docker-action/entrypoint.sh

@@ -117,6 +117,10 @@ if [[ $INPUT_CONDITIONALIZEPERMISSIONS  -eq 1 ]]; then
 	GOBRA_ARGS="$GOBRA_ARGS --conditionalizePermissions"
 fi
 
+if [[ $INPUT_OVERFLOW -eq 1 ]]; then
+	GOBRA_ARGS="$GOBRA_ARGS --overflow"
+fi
+
 if [[ $INPUT_STATSFILE ]]; then
 	# We write the file to /tmp/ (which is easier then making gobra write directly
 	# to the STATS_TARGET, as doing so often causes Gobra to not generate a file) due

entrypoint.sh

@@ -8,7 +8,7 @@ export STATS_TARGET="/stats/"
 
 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_TIMEOUT -e INPUT_HEADERONLY -e INPUT_STATSFILE \
+ -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_PARALLELIZEBRANCHES -e INPUT_CONDITIONALIZEPERMISSIONS -e GITHUB_WORKSPACE -e GITHUB_REPOSITORY \

test/files_test/file2.gobra

@@ -17,6 +17,7 @@ func sum(n int) (sum int) {
 }
 
 ensures res == (n % 2 == 0)
+decreases
 pure func isEven(n int) (res bool) {
 	return n % 2 == 0
 }
@@ -30,4 +31,4 @@ func halfRoundedUp(n int) (res int) {
 		res = n / 2 + 1
 	}
 	return res
-}
+}