Merge pull request #738 from viperproject/meilers_fix_decreases_impor…

…t_post

Also checking postconditions for decreases clauses

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

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