Merge pull request #822 from viperproject/meilers_fix_silicon_886

Added missing variable declaration for checking InEx-Expressions in function postconditions
viperproject · Dec 6, 2024 · f7c9468 · f7c9468
2 parents 3d95d76 + 333014a
commit f7c9468
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 1 deletion.
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
@@ -98,7 +98,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
 
         if (proofMethodBody != EmptyStmt) {
           val proofMethod = Method(proofMethodName, f.formalArgs, Nil, f.pres, Nil,
-            Option(Seqn(Seq(proofMethodBody), Seq(resultVariable))()))(info = f.info)
+            Option(Seqn(Seq(proofMethodBody), Seq(resultVariable, context.conditionInEx.get))()))(info = f.info)
 
           Seq(proofMethod)
         } else {

diff --git a/src/test/resources/all/issues/silicon/0883.vpr b/src/test/resources/all/issues/silicon/0883.vpr
@@ -1,3 +1,7 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
 field f: Int
 
 @moreJoins("2")

diff --git a/src/test/resources/all/issues/silicon/0886.vpr b/src/test/resources/all/issues/silicon/0886.vpr
@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+function foo(): Bool
+  decreases
+
+function bar(): Int
+  decreases
+  ensures [foo(), true]