From 19f9966306adff0ef279a573e2c80f04f8c2b409 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Tue, 2 Apr 2024 14:13:02 +0200
Subject: [PATCH 1/2] add missing termination measures

---
 .../gobra/translator/encodings/arrays/ArrayEncoding.scala     | 4 +++-
 .../translator/encodings/sequences/SequenceEncoding.scala     | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
index 551450ec2..343e66fd4 100644
--- a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
@@ -362,12 +362,14 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         Seq(vpr.Trigger(Seq(trigger))()),
         vpr.Implies(boundaryCondition(vIdx.localVar, t.len)(src), idxEq)()
       )()
+      val terminationMeasure =
+        synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
 
       vpr.Function(
         name = s"${Names.arrayDefaultFunc}_${t.serialize}",
         formalArgs = Seq.empty,
         typ = vResType,
-        pres = Seq.empty,
+        pres = Seq(terminationMeasure),
         posts = Vector(lenEq, arrayEq),
         body = None
       )()
diff --git a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
index cba1ace53..8424c6775 100644
--- a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
@@ -17,6 +17,7 @@ import viper.gobra.translator.util.FunctionGenerator
 import viper.gobra.translator.util.ViperUtil.synthesized
 import viper.gobra.translator.util.ViperWriter.CodeWriter
 import viper.gobra.util.Violation
+import viper.silver.plugin.standard.termination
 import viper.silver.{ast => vpr}
 
 class SequenceEncoding extends LeafTypeEncoding {
@@ -245,6 +246,7 @@ class SequenceEncoding extends LeafTypeEncoding {
 
       // preconditions
       val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), nDecl.localVar))("Sequence length might be negative")
+      val pre2 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
 
       // postconditions
       val post1 = vpr.EqCmp(vResultLength, nDecl.localVar)()
@@ -262,7 +264,7 @@ class SequenceEncoding extends LeafTypeEncoding {
         name = s"${Names.emptySequenceFunc}_${Names.serializeType(t)}",
         formalArgs = Vector(nDecl),
         typ = vResultType,
-        pres = Vector(pre1),
+        pres = Vector(pre1, pre2),
         posts = Vector(post1, post2),
         body = None
       )()

From 3e9cfd849a9a6ef1d7475f3a10788797149eb39c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Tue, 2 Apr 2024 14:53:45 +0200
Subject: [PATCH 2/2] address feedback from pr

---
 .../viper/gobra/translator/encodings/arrays/ArrayEncoding.scala  | 1 +
 .../gobra/translator/encodings/sequences/SequenceEncoding.scala  | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
index 343e66fd4..5eb0a288e 100644
--- a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
@@ -340,6 +340,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * function arrayDefault(): ([n]T)°
     *   ensures len(result) == n
     *   ensures Forall idx :: {result[idx]} 0 <= idx < n ==> [result[idx] == dflt(T)]
+    *   decreases _
     * */
   private val exDfltFunc: FunctionGenerator[ComponentParameter] = new FunctionGenerator[ComponentParameter]{
     def genFunction(t: ComponentParameter)(ctx: Context): vpr.Function = {
diff --git a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
index 8424c6775..cd81a08c0 100644
--- a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
@@ -226,6 +226,7 @@ class SequenceEncoding extends LeafTypeEncoding {
     *   requires 0 <= n
     *   ensures |result| == n
     *   ensures forall i : Int :: { result[i] } 0 <= i < n ==> result[i] == dfltVal(`T`)
+    *   decreases _
     * }}}
     */
   private val emptySeqFunc: FunctionGenerator[in.Type] = new FunctionGenerator[in.Type] {