blob: c1560317a8fd06893dbabcb578679d44309b3381 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file is a series of basic tests for loop detection, focusing on the
// warnings and information messages
function f(i: int): int
function g(i: int): int
method M() {
assert forall i :: false ==> f(i) == f(f(i));
assert forall i :: false ==> f(i) == f(i+1);
assert forall i {:matchingloop} :: false ==> f(i) == f(i+1);
assert forall i :: false ==> f(i) == f(i+1) && f(i) == g(i);
assert forall i :: false ==> f(i) == f(i+1) && f(i) == f(i);
assert forall i {:matchingloop} :: false ==> f(i) == f(i+1) && f(i) == f(i);
assert forall i :: false ==> f(i) == 0;
assert forall i :: false ==> f(i+1) == 0;
assert forall i {:autotriggers false} :: false ==> f(i+1) == 0;
assert forall i, j: int :: false ==> f(i) == f(j);
assert forall i, j: int :: false ==> f(i) == f(i);
assert forall i, j: int :: false ==> f(i) == f(i) && g(j) == 0;
assert forall i, j: int :: false ==> f(i) == f(i) && g(j+1) == 0;
assert forall i, j: int {:autotriggers false} :: false ==> f(i) == f(i);
assert forall i, j: int {:trigger f(i), g(j)} :: false ==> f(i) == f(i);
}
|