From 7681cd7f696182c206654eea01c90bfc9b9973ce Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 25 Aug 2023 16:17:54 +0200 Subject: [PATCH] Also checking postconditions for decreases for autoimport and predicate transformation --- .../plugin/standard/termination/TerminationPlugin.scala | 6 +++--- .../termination/functions/existingExamples/LinkedLists.sil | 2 +- 2 files changed, 4 insertions(+), 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 index 85ed54c2d..d7b2754a9 100644 --- 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 index 905741c51..091be4b69 100644 --- 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