diff options
Diffstat (limited to 'Test/aitest1/ineq.bpl')
| -rw-r--r-- | Test/aitest1/ineq.bpl | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/Test/aitest1/ineq.bpl b/Test/aitest1/ineq.bpl new file mode 100644 index 00000000..a417aaf3 --- /dev/null +++ b/Test/aitest1/ineq.bpl @@ -0,0 +1,81 @@ +// Test the polyhedra domain for linear inequalities
+
+
+procedure SimpleLoop ()
+{
+ var i : int;
+
+ start:
+ i := 0;
+ goto test;
+
+ test:
+ goto Then, Else;
+
+ Then:
+ assume i < 10;
+ i := i + 1;
+ goto test;
+
+ Else:
+ assume ! (i < 10);
+ return;
+}
+
+
+procedure VariableBoundLoop (n : int)
+{
+ var i : int;
+
+ start:
+ i := 0;
+ goto test;
+
+ test:
+ goto Then, Else;
+
+ Then:
+ assume i < n;
+ i := i + 1;
+ goto test;
+
+ Else:
+ assume ! (i < n);
+ return;
+}
+
+procedure Foo ()
+{
+ var i : int;
+
+ start:
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3 ;
+ return;
+}
+
+procedure FooToo ()
+{
+ var i : int;
+
+ start:
+ i := 5;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3 ;
+ return;
+}
+
+procedure FooTooStepByStep ()
+{
+ var i : int;
+
+ L0: i := 5; goto L1;
+ L1: i := 3 * i + 1; goto L2;
+ L2: i := 3 * (i + 1); goto L3;
+ L3: i := 1 + 3 * i; goto L4;
+ L4: i := (i + 1) * 3; return;
+}
|