Also checking postconditions for decreases for autoimport and predica…

…te transformation
viperproject · Aug 25, 2023 · 7681cd7 · 7681cd7
1 parent 56b74d1
commit 7681cd7
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -104,10 +104,10 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
         decreasesClauses = decreasesClauses :+ dc
         dc
       case d => d
-    }).recurseFunc({ // decreases clauses can only appear in functions/methods pres and methods bodies
+    }).recurseFunc({ // decreases clauses can only appear in functions/methods pres, posts and methods bodies
       case PProgram(_, _, _, _, functions, _, methods, _, _) => Seq(functions, methods)
-      case PFunction(_, _, _, pres, _, _) => Seq(pres)
-      case PMethod(_, _, _, pres, _, body) => Seq(pres, body)
+      case PFunction(_, _, _, pres, posts, _) => Seq(pres, posts)
+      case PMethod(_, _, _, pres, posts, body) => Seq(pres, posts, body)
     }).execute(input)
 
     newProgram

diff --git a/src/test/resources/termination/functions/existingExamples/LinkedLists.sil b/src/test/resources/termination/functions/existingExamples/LinkedLists.sil
@@ -11,9 +11,9 @@ predicate list(xs: Ref) {
 }
 
 function length(xs: Ref): Int
-  decreases list(xs)
   requires acc(list(xs)) && xs != null // (1)
   ensures result > 0
+  decreases list(xs)
 { unfolding acc(list(xs)) in 1 + (xs.next == null ? 0 : length(xs.next)) } // (1)
 
 function sum(xs: Ref): Int