Missing termination measures (#675)

* sadd termination * sliceconstruct termination measure * change dummy comment in synthesized
viperproject · Sep 14, 2023 · 86529bc · 86529bc
1 parent 5b178fc
commit 86529bc
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
@@ -342,6 +342,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
     *   ensures soffset(result) == offset
     *   ensures slen(result) == len
     *   ensures scap(result) == cap
+    *   dereases _
     * }}}
     */
   private val constructGenerator : FunctionGenerator[vpr.Type] = new FunctionGenerator[vpr.Type] {
@@ -357,6 +358,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
       val pre2 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), lenDecl.localVar))("Slice length might be negative")
       val pre3 = synthesized(vpr.LeCmp(lenDecl.localVar, capDecl.localVar))("Slice length might exceed capacity")
       val pre4 = synthesized(vpr.LeCmp(vpr.Add(offsetDecl.localVar, capDecl.localVar)(), ctx.array.len(aDecl.localVar)()))("Slice capacity might exceed the capacity of the underlying array")
+      val pre5 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
 
       // postconditions
       val result = vpr.Result(ctx.slice.typ(typ))()
@@ -369,7 +371,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
         s"${Names.sliceConstruct}_${Names.serializeType(typ)}",
         Seq(aDecl, offsetDecl, lenDecl, capDecl),
         ctx.slice.typ(typ),
-        Seq(pre1, pre2, pre3, pre4),
+        Seq(pre1, pre2, pre3, pre4, pre5),
         Seq(post1, post2, post3, post4),
         None
       )()

diff --git a/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala b/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala
@@ -7,6 +7,8 @@
 package viper.gobra.translator.library.slices
 
 import viper.gobra.translator.library.arrays.Arrays
+import viper.silver.plugin.standard.termination
+import viper.gobra.translator.util.ViperUtil.synthesized
 import viper.silver.{ast => vpr}
 
 class SlicesImpl(val arrays : Arrays) extends Slices {
@@ -274,6 +276,7 @@ class SlicesImpl(val arrays : Arrays) extends Slices {
     * {{{
     * function sadd(left: Int, right: Int): Int
     *   ensures result == left + right
+    *   decreases
     * {
     *   left + right
     * }
@@ -284,7 +287,8 @@ class SlicesImpl(val arrays : Arrays) extends Slices {
     val rDecl = vpr.LocalVarDecl("right", vpr.Int)()
     val body : vpr.Exp = vpr.Add(lDecl.localVar, rDecl.localVar)()
     val post : vpr.Exp = vpr.EqCmp(vpr.Result(vpr.Int)(), body)()
-    vpr.Function("sadd", Seq(lDecl, rDecl), vpr.Int, Seq(), Seq(post), Some(body))()
+    val pre  : vpr.Exp = synthesized(termination.DecreasesTuple(Seq.empty, None))("Termination measure")
+    vpr.Function("sadd", Seq(lDecl, rDecl), vpr.Int, Seq(pre), Seq(post), Some(body))()
   }
 
   /**