Issue #783

src/main/resources/stubs/strconv/atoi.gobra

@@ -42,10 +42,11 @@ pure func (e *NumError) Unwrap() error { return e.Err }
 
 // a to the power of b
 ghost
+requires base == 0 || (2 <= base && base <= 36)
 requires exp >= 0
 ensures res == (exp == 0 ? 1 : (base * Exp(base, exp - 1)))
 decreases exp
-pure func Exp(base int, exp int) (res int) {
+pure func Exp(base uint64, exp int) (res uint64) {
 	return exp == 0 ? 1 : (base * Exp(base, exp - 1))
 }
 

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -180,7 +180,7 @@ object Desugar extends LazyLogging {
     }
   }
 
-  private class Desugarer(pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo, initSpecs: PackageInitSpecCollector) {
+  private class Desugarer(@unused pom: PositionManager, info: viper.gobra.frontend.info.TypeInfo, initSpecs: PackageInitSpecCollector) {
 
     type Meta = Source.Parser.Info
 

src/main/scala/viper/gobra/frontend/info/base/Type.scala

@@ -41,8 +41,12 @@ object Type {
 
   case class IntT(kind: TypeBounds.IntegerKind) extends PrettyType(kind.name)
 
-  case object Float32T extends PrettyType("float32")
-  case object Float64T extends PrettyType("float64")
+  trait FloatT extends PrettyType
+  /** type for floating point numbers with unbounded precision */
+  case object UnboundedFloatT extends PrettyType("unbounded float") with FloatT
+  trait TypedFloatT extends FloatT
+  case object Float32T extends PrettyType("float32") with TypedFloatT
+  case object Float64T extends PrettyType("float64") with TypedFloatT
 
   case class ArrayT(length: BigInt, elem: Type) extends PrettyType(s"[$length]$elem") {
     require(length >= 0, "The length of an array must be non-negative")

src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala

@@ -53,6 +53,7 @@ class TypeInfoImpl(final val tree: Info.GoTree, override final val dependentType
   with Assignability
   with Addressability
   with TypeIdentity
+  with Orderability
   with PointsTo
   with Executability
   with ConstantEvaluation

src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala

@@ -110,6 +110,8 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
       case (UNTYPED_INT_CONST, r) if underlyingType(r).isInstanceOf[IntT] => successProp
       // not part of Go spec, but necessary for the definition of comparability
       case (l, UNTYPED_INT_CONST) if underlyingType(l).isInstanceOf[IntT] => successProp
+      case (UNTYPED_INT_CONST, r) if underlyingType(r).isInstanceOf[FloatT] => successProp
+      case (UnboundedFloatT, r) if underlyingType(r).isInstanceOf[FloatT] => successProp
       case (l, r) if identicalTypes(l, r) => successProp
       // the go language spec states that a value x of type V is assignable to a variable of type T
       // if V and T have identical underlying types and at least one of V or T is not a defined type

src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala

@@ -6,7 +6,7 @@
 
 package viper.gobra.frontend.info.implementation.property
 
-import viper.gobra.frontend.info.base.Type.{ActualPointerT, DeclaredT, Float32T, Float64T, GhostPointerT, IntT, PermissionT, Single, SliceT, StringT, Type}
+import viper.gobra.frontend.info.base.Type.{ActualPointerT, DeclaredT, Float32T, Float64T, FloatT, GhostPointerT, IntT, PermissionT, Single, SliceT, StringT, Type}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 trait Convertibility extends BaseProperty { this: TypeInfoImpl =>
@@ -25,8 +25,7 @@ trait Convertibility extends BaseProperty { this: TypeInfoImpl =>
           s"of this current package.")
       case (IntT(_), Float32T) => successProp
       case (IntT(_), Float64T) => successProp
-      case (Float32T, IntT(_)) => successProp
-      case (Float64T, IntT(_)) => successProp
+      case (_: FloatT, IntT(_)) => successProp
       case (IntT(_), IntT(_)) => successProp
       case (SliceT(IntT(config.typeBounds.Byte)), StringT) => successProp
       case (StringT, SliceT(IntT(config.typeBounds.Byte))) => successProp

src/main/scala/viper/gobra/frontend/info/implementation/property/Orderability.scala

@@ -0,0 +1,24 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2025 ETH Zurich.
+
+package viper.gobra.frontend.info.implementation.property
+
+import viper.gobra.frontend.info.base.Type._
+import viper.gobra.frontend.info.implementation.TypeInfoImpl
+
+trait Orderability extends BaseProperty { this: TypeInfoImpl =>
+
+  lazy val orderedType: Property[Type] = createBinaryProperty("ordered") {
+    case Single(st) => underlyingType(st) match {
+      case _: IntT => true
+      case PermissionT => true
+      case _: FloatT => true
+      case StringT => true
+      case _ => false
+    }
+    case _ => false
+  }
+}

src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala

@@ -6,8 +6,7 @@
 
 package viper.gobra.frontend.info.implementation.property
 
-import viper.gobra.ast.internal.{Float32T, Float64T}
-import viper.gobra.frontend.info.base.Type.{ActualPointerT, ArrayT, AssertionT, BooleanT, ChannelT, GhostPointerT, GhostSliceT, IntT, InternalTupleT, MapT, MultisetT, PermissionT, SequenceT, SetT, Single, SliceT, Type}
+import viper.gobra.frontend.info.base.Type.{ActualPointerT, ArrayT, AssertionT, BooleanT, ChannelT, FloatT, GhostPointerT, GhostSliceT, IntT, InternalTupleT, MapT, MultisetT, PermissionT, SequenceT, SetT, Single, SliceT, Type, UnboundedFloatT}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 trait TypeMerging extends BaseProperty { this: TypeInfoImpl =>
@@ -27,10 +26,10 @@ trait TypeMerging extends BaseProperty { this: TypeInfoImpl =>
 
           case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[IntT] => Some(a)
           case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[IntT] => Some(b)
-          case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float64T] => Some(a)
-          case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float64T] => Some(b)
-          case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float32T] => Some(a)
-          case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float32T] => Some(b)
+          case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[FloatT] => Some(a)
+          case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[FloatT] => Some(b)
+          case (a, UnboundedFloatT) if underlyingType(a).isInstanceOf[FloatT] => Some(a)
+          case (UnboundedFloatT, b) if underlyingType(b).isInstanceOf[FloatT] => Some(b)
           case (BooleanT, AssertionT) => Some(AssertionT)
           case (AssertionT, BooleanT) => Some(AssertionT)
           case (IntT(_), PermissionT) => Some(PermissionT)

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -10,12 +10,14 @@ import org.bitbucket.inkytonik.kiama.util.Message
 import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, check, error, noMessages}
 import viper.gobra.ast.frontend.{AstPattern => ap, _}
 import viper.gobra.frontend.info.base.SymbolTable.{AdtDestructor, AdtDiscriminator, GlobalVariable, SingleConstant}
-import viper.gobra.frontend.info.base.Type._
+import viper.gobra.frontend.info.base.Type.{StringT, _}
 import viper.gobra.frontend.info.base.{SymbolTable => st}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.TypeBounds.{BoundedIntegerKind, UnboundedInteger}
 import viper.gobra.util.{Constants, TypeBounds, Violation}
 
+import scala.annotation.nowarn
+
 trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
   import viper.gobra.util.Violation._
@@ -222,7 +224,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case n: PIota =>
       error(n, s"cannot use iota outside of constant declaration", enclosingPConstDecl(n).isEmpty)
 
-    case _: PFloatLit => ???
+    case n: PFloatLit => error(n, s"floating point literals are not yet supported.")
 
     case n@PCompositeLit(t, lit) =>
       val mayInit = isEnclosingMayInit(n)
@@ -477,22 +479,30 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case n: PBinaryExp[_,_] =>
         val mayInit = isEnclosingMayInit(n)
         (n, exprOrTypeType(n.left), exprOrTypeType(n.right)) match {
-          case (_: PEquals | _: PUnequals, l, r) => comparableTypes.errors(l, r)(n)
-          case (_: PAnd | _: POr, l, r) => assignableTo.errors(l, AssertionT, mayInit)(n.left) ++
-            assignableTo.errors(r, AssertionT, mayInit)(n.right)
-          case (_: PLess | _: PAtMost | _: PGreater | _: PAtLeast, l, r) => (l,r) match {
-            case (StringT, StringT) => noMessages
-            case (Float32T, Float32T) => noMessages
-            case (Float64T, Float64T) => noMessages
-            case _ if l == PermissionT || r == PermissionT =>
-              assignableTo.errors(l, PermissionT, mayInit)(n.left) ++
-                assignableTo.errors(r, PermissionT, mayInit)(n.right)
-            case _ =>
-              assignableTo.errors(l, UNTYPED_INT_CONST, mayInit)(n.left) ++
-                assignableTo.errors(r, UNTYPED_INT_CONST, mayInit)(n.right)
-          }
+          case (_: PEquals | _: PUnequals | _: PLess | _: PAtMost | _: PGreater | _: PAtLeast | _: PAnd | _: POr, l, r) =>
+            // from the spec: "first operand must be assignable to the type of the second operand, or vice versa"
+            val fstAssignable = assignableTo.errors(l, r, mayInit)(n)
+            val sndAssignable = assignableTo.errors(r, l, mayInit)(n)
+            val assignable = if (fstAssignable.isEmpty || sndAssignable.isEmpty) noMessages
+              else error(n, s"neither operand is assignable to the type of the other operand")
+            @nowarn("msg=not.*?exhaustive")
+            val applicable = if (assignable.isEmpty) {
+              n match {
+                case _: PEquals | _: PUnequals =>
+                  // from the spec: "The equality operators == and != apply to operands of comparable types"
+                  comparableTypes.errors(l, r)(n)
+                case _: PLess | _: PAtMost | _: PGreater | _: PAtLeast =>
+                  // from the spec: "The ordering operators <, <=, >, and >= apply to operands of ordered types"
+                  orderedType.errors(l)(n.left) ++ orderedType.errors(r)(n.right)
+                case _: PAnd | _: POr =>
+                  // from the spec: "Logical operators apply to boolean values", which we extend from boolean to assertion values:
+                  assignableTo.errors(l, AssertionT, mayInit)(n.left) ++
+                    assignableTo.errors(r, AssertionT, mayInit)(n.right)
+              }
+            } else noMessages
+            assignable ++ applicable
           case (_: PAdd, StringT, StringT) => noMessages
-          case (_: PAdd | _: PSub | _: PMul | _: PDiv, l, r) if Set(l, r).intersect(Set(Float32T, Float64T)).nonEmpty =>
+          case (_: PAdd | _: PSub | _: PMul | _: PDiv, l, r) if Set(l, r).intersect(Set(UnboundedFloatT, Float32T, Float64T)).nonEmpty =>
             mergeableTypes.errors(l, r)(n)
           case (_: PAdd | _: PSub | _: PMul | _: PMod | _: PDiv, l, r)
             if l == PermissionT || r == PermissionT || getTypeFromCtxt(n).contains(PermissionT) =>
@@ -680,7 +690,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
   }
 
   private def numExprWithinTypeBounds(num: PNumExpression): Messages =
-    intExprWithinTypeBounds(num, intExprType(num))
+    intExprWithinTypeBounds(num, numExprType(num))
 
   private def intExprWithinTypeBounds(exp: PExpression, typ: Type): Messages = {
     if (typ == UNTYPED_INT_CONST) {
@@ -711,6 +721,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PBoolLit => BooleanT
     case _: PNilLit => NilType
     case _: PStringLit => StringT
+    case _: PFloatLit => UnboundedFloatT
 
     case cl: PCompositeLit => expectedCompositeLitType(cl)
 
@@ -797,7 +808,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PCapacity => INT_TYPE
 
     case exprNum: PNumExpression =>
-      val typ = intExprType(exprNum)
+      val typ = numExprType(exprNum)
       if (typ == UNTYPED_INT_CONST) getNonInterfaceTypeFromCtxt(exprNum).getOrElse(typ) else typ
 
     case n: PUnfolding => exprType(n.op)
@@ -1058,10 +1069,12 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case _ => violation("blank identifier always has a parent")
   }
 
-  private def intExprType(expr: PNumExpression): Type = {
+  private def numExprType(expr: PNumExpression): Type = {
     val typ = expr match {
       case _: PIntLit => UNTYPED_INT_CONST
 
+      case _: PFloatLit => UnboundedFloatT
+
       case e: PLength => typeOfPLength(e)
 
       case _: PCapacity => INT_TYPE

src/test/resources/regressions/features/integers/int-assign-fail2.gobra

@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package ints
+
+func test1() {
+	var j uint16
+	for i := 0; i < 256; i++ {
+	    //:: ExpectedOutput(type_error)
+		if i < j { // Go compiler reports "invalid operation: i < j (mismatched types int and uint16)"
+			j = 42
+		}
+	}
+}
+
+func test2() {
+    invariant 0 <= i && i <= 256
+    //:: ExpectedOutput(type_error)
+    invariant forall j uint16 :: 0 <= j && j < i ==> true
+    decreases 256 - i
+    for i := 0; i < 256; i++ {}
+}

src/test/resources/regressions/issues/000783-1.gobra

@@ -0,0 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue783_1
+
+//:: ExpectedOutput(type_error)
+requires x > 0.0
+//:: ExpectedOutput(type_error)
+ensures  res > 0.0
+ensures  false
+func newton(x float32, y float32) (res float32) {
+	return x/2 + y / 2 / x
+}

src/test/resources/regressions/issues/000783-2.gobra

@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue783_2
+
+func main() {
+    //:: ExpectedOutput(type_error)
+	assert 1e2 > 0
+	assert false
+}

src/test/resources/regressions/issues/000783-3.gobra

@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue783_3
+
+ensures false
+func floatfn3(f float64) float64 {
+    //:: ExpectedOutput(type_error)
+    return 0.0
+}

src/test/resources/same_package/pkg_init/byte/byte.go

@@ -13,9 +13,9 @@ var byteCache /*@@@*/ [256]*Byte
 
 func init() {
 	// @ invariant 0 <= i && i <= 256 && acc(&byteCache)
-	// @ invariant (forall j, k uint16 :: 0 <= j && j < k && k < i  ==>
+	// @ invariant (forall j, k int :: 0 <= j && j < k && k < i  ==>
 	// @ 	byteCache[j] != byteCache[k])
-	// @ invariant (forall j uint16 :: 0 <= j && j < i ==>
+	// @ invariant (forall j int :: 0 <= j && j < i ==>
 	// @ 	acc(byteCache[j]) && byteCache[j].value == byte(j) - 128)
 	// @ decreases 256 - i
 	for i := 0; i < 256; i++ {