marks permissions as being ordered

Author: ArquintL

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

@@ -6,7 +6,7 @@
 
 package viper.gobra.frontend.info.implementation.property
 
-import viper.gobra.ast.internal.StringT
+import viper.gobra.ast.internal.{PermissionT, StringT}
 import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
@@ -15,6 +15,7 @@ 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

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

@@ -16,6 +16,8 @@ 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._
@@ -479,19 +481,20 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
         (n, exprOrTypeType(n.left), exprOrTypeType(n.right)) match {
           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(exprOrTypeType(n.left), exprOrTypeType(n.right), mayInit)(n)
-            val sndAssignable = assignableTo.errors(exprOrTypeType(n.right), exprOrTypeType(n.left), mayInit)(n)
+            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, exprOrTypeType(n.left), exprOrTypeType(n.right)) match {
-                case (_: PEquals | _: PUnequals, l, r) =>
+              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, l, r) =>
+                case _: PLess | _: PAtMost | _: PGreater | _: PAtLeast =>
                   // from the spec: "The ordering operators <, <=, >, and >= apply to operands of ordered types"
-                  orderedType.errors(l)(n) ++ orderedType.errors(r)(n)
-                case (_: PAnd | _: POr, l, r) =>
+                  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)

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/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++ {