termination

viperproject · Sep 13, 2023 · fa0a0d4 · fa0a0d4
1 parent 21bd69f
commit fa0a0d4
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
@@ -509,6 +509,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
     *   ensures slen(result) == j - i
     *   ensures scap(result) == alen(a) - i
     *   ensures sarray(result) == a
+    *   decreases _
     * {
     *   sfullSliceFromArray(a, i, j, alen(a))
     * }
@@ -525,6 +526,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
       val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDecl.localVar))("The low bound of the slice might be negative")
       val pre2 = synthesized(vpr.LeCmp(iDecl.localVar, jDecl.localVar))("The low bound of the slice might exceed the high bound")
       val pre3 = synthesized(vpr.LeCmp(jDecl.localVar, ctx.array.len(aDecl.localVar)()))("The high bound of the slice might exceed the array capacity")
+      val pre4 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
 
       // postconditions
       val result = vpr.Result(ctx.slice.typ(typ))()
@@ -545,7 +547,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
         s"${Names.sliceFromArray}_${Names.serializeType(typ)}",
         Seq(aDecl, iDecl, jDecl),
         ctx.slice.typ(typ),
-        Seq(pre1, pre2, pre3),
+        Seq(pre1, pre2, pre3, pre4),
         Seq(post1, post2, post3, post4),
         if (generateFunctionBodies) Some(body) else None
       )()