From b3d4f1582b97637514d975e90f8b195f661706d3 Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Thu, 14 Sep 2023 16:38:41 +0200
Subject: [PATCH 1/3] sadd termination

---
 .../viper/gobra/translator/library/slices/SlicesImpl.scala  | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala b/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala
index f614ab63c..ac2340f6a 100644
--- 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))("This function is assumed to terminate")
+    vpr.Function("sadd", Seq(lDecl, rDecl), vpr.Int, Seq(pre), Seq(post), Some(body))()
   }
 
   /**

From 4d73949ea5ec0859669f58acbf2b0c85773de55b Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Thu, 14 Sep 2023 16:43:33 +0200
Subject: [PATCH 2/3] sliceconstruct termination measure

---
 .../gobra/translator/encodings/slices/SliceEncoding.scala     | 4 +++-
 1 file changed, 3 insertions(+), 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
index 7dc2c151f..5590c54f7 100644
--- 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
       )()

From 0ab9faad45be5de06d89a6d1373f1b549ff84d59 Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Thu, 14 Sep 2023 17:08:20 +0200
Subject: [PATCH 3/3] change dummy comment in synthesized

---
 .../viper/gobra/translator/library/slices/SlicesImpl.scala      | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala b/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala
index ac2340f6a..aa1840cb6 100644
--- a/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala
+++ b/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala
@@ -287,7 +287,7 @@ 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)()
-    val pre  : vpr.Exp = synthesized(termination.DecreasesTuple(Seq.empty, None))("This function is assumed to terminate")
+    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))()
   }