Fix bounds of singed integers for overflow checking (#795)

* add example of bug

* fix bug

* fix

src/main/scala/viper/gobra/util/TypeBounds.scala

@@ -43,8 +43,8 @@ object TypeBounds {
   }
 
   sealed trait Signed extends BoundedIntegerKind {
-    override lazy val upper: BigInt = BigInt(pow(2, nbits-1).toLong - 1)
-    override lazy val lower: BigInt = BigInt(-pow(2, nbits-1).toLong)
+    override lazy val upper: BigInt = BigInt(2).pow(nbits-1) - 1
+    override lazy val lower: BigInt = -BigInt(2).pow(nbits-1)
   }
 
   sealed trait Unsigned extends BoundedIntegerKind {

src/test/resources/regressions/features/overflow_checks/overflow_simple1.go

@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+// ##(--overflow)
+
+const MinInt64 = -9223372036854775808 // = -1 << 63
+// @ requires x > MinInt64
+// @ ensures res >= 0
+func abs(x int64) (res int64) {
+	if x < 0 {
+		return -x
+	} else {
+		return x
+	}
+}