From 97f0988cca5c63e10d3a71b6f9e945b83b7c27aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Sat, 16 Nov 2024 10:51:07 +0100
Subject: [PATCH] Fix bounds of singed integers for overflow checking (#795)

* add example of bug

* fix bug

* fix
---
 .../scala/viper/gobra/util/TypeBounds.scala     |  4 ++--
 .../overflow_checks/overflow_simple1.go         | 17 +++++++++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/regressions/features/overflow_checks/overflow_simple1.go

diff --git a/src/main/scala/viper/gobra/util/TypeBounds.scala b/src/main/scala/viper/gobra/util/TypeBounds.scala
index 2682ce845..19e97c44e 100644
--- a/src/main/scala/viper/gobra/util/TypeBounds.scala
+++ b/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 {
diff --git a/src/test/resources/regressions/features/overflow_checks/overflow_simple1.go b/src/test/resources/regressions/features/overflow_checks/overflow_simple1.go
new file mode 100644
index 000000000..4e9c6d025
--- /dev/null
+++ b/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
+	}
+}