summaryrefslogtreecommitdiff
path: root/Test/test0/Triggers1.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test0/Triggers1.bpl')
-rw-r--r--Test/test0/Triggers1.bpl258
1 files changed, 129 insertions, 129 deletions
diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl
index 12d734be..7ab1c191 100644
--- a/Test/test0/Triggers1.bpl
+++ b/Test/test0/Triggers1.bpl
@@ -1,129 +1,129 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// 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 (disabled unless both have no triggers)
-
-axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK, but no merging - outer quantifier has no trigger
-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)); // OK - no merging
-
-// three levels
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error - z not mentioned
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // OK - only outer two quantifiers are merged
-//axiom (forall x:int :: (forall y:int :: (forall z:int :: f(y,y) > 0))); // OK - all three are merged
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK - but not a trigger for outer x,y (which get merged)
-
-// --- 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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// 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 (disabled unless both have no triggers)
+
+axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK, but no merging - outer quantifier has no trigger
+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)); // OK - no merging
+
+// three levels
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error - z not mentioned
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // OK - only outer two quantifiers are merged
+//axiom (forall x:int :: (forall y:int :: (forall z:int :: f(y,y) > 0))); // OK - all three are merged
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK - but not a trigger for outer x,y (which get merged)
+
+// --- 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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 08:24:20 +0000