summaryrefslogtreecommitdiff
path: root/Test/test0/Triggers1.bpl
blob: 02c6340657e290f221025a219423fec240c743dd (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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
// Trigger errors

function f(int, int) returns (int);
function P(int, int) returns (bool);

axiom (forall x: int ::
       { f(x,10) && f(x,9) }   // error: && not allowed
       f(x,10) == 3);

axiom (forall x: int ::
       { ((((f(x,10) || f(x,9))))) }   // error: || not allowed
       f(x,10) == 3);

axiom (forall x: int ::
       { !f(x,10) }   // error: ! not allowed
       f(x,10) == 3);

axiom (forall x: int ::
       { (!f(x,10)) }   // error: ! not allowed
       f(x,10) == 3);

axiom (forall x: int ::
       { P(x,10) ==> P(20,x) }   // error: ==> not allowed
       f(x,10) == 3);

axiom (forall x: int ::
       { P(x,10) <==> P(20,x) }   // error: <==> not allowed
       f(x,10) == 3);


axiom (forall x: int ::
       { f(x,10) == 3 }   // error: == not allowed
       f(x,10) == 3);

axiom (forall x: int ::
       { f(x,10) < 3 }   // error: < not allowed
       f(x,10) == 3);


axiom (forall x: int ::
       { f(x,10) + f(x,x) != 3 }   // yes, != is allowed
       f(x,10) == 3);

axiom (forall b: bool ::
       { (forall y: int :: b) }   // error: quantifiers not allowed
       b);

// -------------- tests of free variables

const g: int;

axiom (forall x: int ::
       { false, 6 }             // error: does not mention "x"
       x < x + 1);

axiom (forall x: int ::
       { false, x+1, 6 }        // allowed
       x < x + 1);

axiom (forall x: int, y: int ::
       { x+1 }                  // error: does not mention "y"
       { y+1 }                  // error: does not mention "x"
       x < y + 1);

axiom (forall x: int ::
       { g+x != 65 }            // allowed
       x < x + 1);

axiom (forall x: int ::
       { x }                    // "x" by itself is not a good trigger
       x < x + 1);

//axiom (forall x: any ::  // PR: removed for the time being
//       { cast(x,int) }          // can't fool me, still not allowed
//       x == x );

// --- multiple triggers

axiom (forall x: int, y: int, z: int ::
       { x+y+z }                // good
       { x+y, y+z }             // also good
       { f(f(x,y),y) }          // error: does not mention z
       x == x );

// --- multi-triggers

axiom (forall x: int, y: int, z: int ::
       { f(x,x), f(y,y), f(z,z) }  // good
       f(x,y) < f(y,z) );

// --- pattern exclusion

axiom (forall x: int, y: int ::
       {:nopats x }                   // error: "x" by itself is not allowed here either
       {:nopats g }                   // error: "g" by itself is not allowed here either
       x < y);

axiom (forall x: int, y: int ::
       {:nopats f(g,g) }              // but it is okay not to mention the bound variables (in a pattern exclusion)
       x < y);

// --- merging of nested quantifiers

axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK
axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error
axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // error

// three levels
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // error
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(y,z) } f(y,y) > 0))); // error
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK

// --- no free variables

var h0: int;
var h1: [ref,ref]int;

axiom (forall o: ref, f: ref  :: h1[o,f] // error: cannot mention free variable "h1"
                               < h0);    // error: cannot mention free variable "h0"

const c0: int;
const c1: [ref,ref]int;

axiom (forall o: ref, f: ref :: c1[o,f] < c0);

type ref;