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 + } +}