Skip to content

Commit 3522af7

Browse files
committed
Merge branch 'meilers_term_plugin_deactive_flag' of https://github.com/viperproject/silver into meilers_term_plugin_deactive_flag
2 parents d52e42f + 4f4f990 commit 3522af7

3 files changed

Lines changed: 49 additions & 0 deletions

File tree

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
140140
case PMapType(_, _) => Seq("Map")
141141
case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances")
142142
case PDomainType(d, _) => Seq(d.name)
143+
case gt: PGenericType => Seq(gt.genericName)
143144
}
144145
!typeNames.exists(tn => wfTypeName.contains(tn))
145146
}
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Any copyright is dedicated to the Public Domain.
2+
// http://creativecommons.org/publicdomain/zero/1.0/
3+
4+
5+
field f: Bool
6+
7+
method fails(a: Bool)
8+
{
9+
var curr: Ref := null
10+
11+
while (curr != null)
12+
invariant curr != null ==> acc(curr.f)
13+
{
14+
refute false
15+
curr := null
16+
}
17+
18+
//:: ExpectedOutput(assert.failed:assertion.false)
19+
assert false
20+
}
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// Any copyright is dedicated to the Public Domain.
2+
// http://creativecommons.org/publicdomain/zero/1.0/
3+
4+
import <decreases/all.vpr>
5+
6+
domain ListWellFoundedOrder[T] {
7+
8+
9+
axiom {
10+
forall y : List[T] :: {bounded(y)} bounded(y)
11+
}
12+
13+
14+
axiom {
15+
forall xs : List[T] , y : T ::
16+
decreasing(xs, Cons(y, xs))
17+
}
18+
19+
axiom {
20+
forall xs : List[T], ys : List[T], zs : List[T] :: {decreasing(xs, ys), decreasing(ys, zs)}
21+
decreasing(xs, ys) && decreasing(ys, zs) ==> decreasing(xs, zs)
22+
}
23+
}
24+
25+
adt List[T] {
26+
Nil()
27+
Cons(value : T, tail : List[T])
28+
}

0 commit comments

Comments
 (0)