Merge branch 'master' into ghost-pointer

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 = {
@@ -362,12 +363,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
       )()

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 {
@@ -225,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] {
@@ -245,6 +247,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 +265,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
       )()

src/main/scala/viper/gobra/util/ChopperUtil.scala

@@ -91,6 +91,7 @@ object ChopperUtil {
         method          = get("method_body",      dfltConf.method),
         methodSpec      = get("method_spec",      dfltConf.methodSpec),
         function        = get("function_body",    dfltConf.function),
+        functionSig     = get("function_spec",    dfltConf.function),
         predicate       = get("predicate_body",   dfltConf.predicate),
         predicateSig    = get("predicate_spec",   dfltConf.predicateSig),
         field           = get("field",            dfltConf.field),