From bfdf70b13df618129577bfcd5f93d7bd0eed2493 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 14 Aug 2023 19:05:38 +0200 Subject: [PATCH 1/2] Added missing case (fixes Silicon issue #742) --- .../silver/plugin/standard/termination/TerminationPlugin.scala | 1 + 1 file changed, 1 insertion(+) 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 2c9d2427e..85ed54c2d 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala @@ -140,6 +140,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter, case PMapType(_, _) => Seq("Map") case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances") case PDomainType(d, _) => Seq(d.name) + case gt: PGenericType => Seq(gt.genericName) } !typeNames.exists(tn => wfTypeName.contains(tn)) } From 948b7e9265b5a245ff6e8f16993d26fc34ea99d9 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 14 Aug 2023 19:51:00 +0200 Subject: [PATCH 2/2] Added test case --- .../resources/all/issues/silicon/0742.vpr | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 src/test/resources/all/issues/silicon/0742.vpr diff --git a/src/test/resources/all/issues/silicon/0742.vpr b/src/test/resources/all/issues/silicon/0742.vpr new file mode 100644 index 000000000..767bbd458 --- /dev/null +++ b/src/test/resources/all/issues/silicon/0742.vpr @@ -0,0 +1,28 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +import + +domain ListWellFoundedOrder[T] { + + + axiom { + forall y : List[T] :: {bounded(y)} bounded(y) + } + + + axiom { + forall xs : List[T] , y : T :: + decreasing(xs, Cons(y, xs)) + } + + axiom { + forall xs : List[T], ys : List[T], zs : List[T] :: {decreasing(xs, ys), decreasing(ys, zs)} + decreasing(xs, ys) && decreasing(ys, zs) ==> decreasing(xs, zs) + } +} + +adt List[T] { + Nil() + Cons(value : T, tail : List[T]) +} \ No newline at end of file