diff options
Diffstat (limited to 'Chalice/tests/regressions/workitem-10189.chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10189.chalice | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice new file mode 100644 index 00000000..b37b83f2 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10189.chalice @@ -0,0 +1,23 @@ +class Node { + var v: int + var next: Node + + predicate V { + acc(v) + && acc(next) + && (next != null ==> next.V) + } + + unlimited function length(): int + requires rd(V) + { 1 + unfolding rd(V) in next == null ? 0 : next.length() } + + unlimited function at(i: int): int + requires rd(V) + requires i >= 0 + requires i < length() // XXXX + { + unfolding rd(V) in i == 0 ? v : next.at(i - 1) + // Precondition at XXX might not hold + } +}
\ No newline at end of file |