Fix issue 621 (#622)

* Fix 621 * fix identation
viperproject · Feb 10, 2023 · e498930 · e498930
1 parent 64122cf
commit e498930
Show file tree

Hide file tree

Showing 11 changed files with 33 additions and 10 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
@@ -15,7 +15,6 @@ import viper.gobra.frontend.info.base.Type
 import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.BaseTyping
-import viper.gobra.util.TypeBounds
 import viper.gobra.util.Violation.violation
 
 import scala.annotation.unused

diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
@@ -17,8 +17,10 @@ import viper.gobra.translator.encodings.combinators.TypeEncoding
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.library.embeddings.EmbeddingParameter
 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}
 
 import scala.annotation.unused
@@ -318,7 +320,10 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         name = s"${Names.arrayConversionFunc}_${t.serialize}",
         formalArgs = Vector(variable(ctx)(x)),
         typ = vResultType,
-        pres = Vector(pure(addressFootprint(ctx)(x, in.WildcardPerm(Source.Parser.Internal)))(ctx).res),
+        pres = Vector(
+          pure(addressFootprint(ctx)(x, in.WildcardPerm(Source.Parser.Internal)))(ctx).res,
+          synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
+        ),
         posts = Vector(post),
         body = None
       )()

diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponentImpl.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/SharedArrayComponentImpl.scala
@@ -15,7 +15,9 @@ import viper.gobra.translator.context.Context
 import viper.gobra.translator.library.embeddings.EmbeddingComponent
 import viper.gobra.translator.Names
 import viper.gobra.translator.util.FunctionGenerator
+import viper.gobra.translator.util.ViperUtil.synthesized
 import viper.gobra.translator.util.ViperWriter.CodeLevel.pure
+import viper.silver.plugin.standard.termination
 
 class SharedArrayComponentImpl extends SharedArrayComponent {
 
@@ -48,7 +50,7 @@ class SharedArrayComponentImpl extends SharedArrayComponent {
         name = s"${Names.arrayNilFunc}_${t.serialize}",
         formalArgs = Seq.empty,
         typ = vResType,
-        pres = Seq.empty,
+        pres = Seq(synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")),
         posts = Vector(vpr.EqCmp(ctx.array.len(vpr.Result(vResType)())(), vpr.IntLit(1)())(), forall),
         body = None
       )()

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -443,8 +443,4 @@ trait TypeEncoding extends Generator {
     val (pos, info, errT) = src.vprMeta
     node(pos, info, errT)(ctx)
   }
-
-  /** Adds simple (source) information to a node without source information. */
-  protected def synthesized[T](node: (vpr.Position, vpr.Info, vpr.ErrorTrafo) => T)(comment: String): T =
-    node(vpr.NoPosition, vpr.SimpleInfo(Seq(comment)), vpr.NoTrafos)
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultGlobalVarEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultGlobalVarEncoding.scala
@@ -10,6 +10,7 @@ import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.encodings.combinators.Encoding
+import viper.gobra.translator.util.ViperUtil.synthesized
 import viper.gobra.translator.util.ViperWriter.MemberLevel.unit
 import viper.gobra.translator.util.ViperWriter.MemberWriter
 import viper.silver.{ast => vpr}

diff --git a/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/sequences/SequenceEncoding.scala
@@ -14,6 +14,7 @@ import viper.gobra.translator.Names
 import viper.gobra.translator.encodings.combinators.LeafTypeEncoding
 import viper.gobra.translator.context.Context
 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.{ast => vpr}

diff --git a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
@@ -17,6 +17,7 @@ import viper.gobra.translator.encodings.arrays.SharedArrayEmbedding
 import viper.gobra.translator.encodings.combinators.LeafTypeEncoding
 import viper.gobra.translator.context.Context
 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.verifier.{errors => err}

diff --git a/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala
@@ -14,6 +14,7 @@ import viper.gobra.translator.Names
 import viper.gobra.translator.encodings.combinators.TypeEncoding
 import viper.gobra.translator.context.Context
 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.{ast => vpr}

diff --git a/src/main/scala/viper/gobra/translator/library/embeddings/EmbeddingComponent.scala b/src/main/scala/viper/gobra/translator/library/embeddings/EmbeddingComponent.scala
@@ -9,6 +9,7 @@ package viper.gobra.translator.library.embeddings
 import viper.gobra.translator.Names
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.library.Generator
+import viper.gobra.translator.util.ViperUtil.synthesized
 import viper.silver.{ast => vpr}
 import viper.silver.plugin.standard.termination
 
@@ -149,7 +150,4 @@ object EmbeddingComponent {
       genUnboxFuncMap += (id -> unbox)
     }
   }
-
-  private def synthesized[T](node: (vpr.Position, vpr.Info, vpr.ErrorTrafo) => T)(comment: String): T =
-    node(vpr.NoPosition, vpr.SimpleInfo(Seq(comment)), vpr.NoTrafos)
 }
diff --git a/src/main/scala/viper/gobra/translator/util/ViperUtil.scala b/src/main/scala/viper/gobra/translator/util/ViperUtil.scala
@@ -104,4 +104,8 @@ object ViperUtil {
 
     s.reduceWithContext(Nil, addDecls, combineResults)
   }
+
+  /** Adds simple (source) information to a node without source information. */
+  def synthesized[T](node: (Position, Info, ErrorTrafo) => T)(comment: String): T =
+    node(NoPosition, SimpleInfo(Seq(comment)), NoTrafos)
 }
diff --git a/src/test/resources/regressions/issues/000621.gobra b/src/test/resources/regressions/issues/000621.gobra
@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+type A struct {
+	x [3]int
+}
+
+ghost
+requires acc(&a.x)
+decreases
+pure func f(a *A) int {
+	return let x := a.x in x[0]
+}