diff options
| author |  wuestholz <unknown> | 2013-07-12 16:29:30 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-12 16:29:30 -0700 |
| commit | fb7ba0533f976442e53a4180a988ac7e2bb5c777 (patch) | |
| tree | 5ac09f7787d16144c5f08c83da2541aaf55f3f72 /Test/test2 | |
| parent | 714a571fee581fca2c46cf7debd9743ca1095eec (diff) | |
Added an attribute to set the time limit for implementations.
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/Answer | 44 | ||||
| -rw-r--r-- | Test/test2/Timeouts0.bpl | 58 |
2 files changed, 100 insertions, 2 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5f8642e1..e9390250 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -502,5 +502,45 @@ Execution trace: Timeouts0.bpl(10,5): anon4_LoopDone
Timeouts0.bpl(19,5): anon5_LoopHead
Timeouts0.bpl(23,11): anon5_LoopBody
-
-Boogie program verifier finished with 0 verified, 0 errors, 1 time out
+Timeouts0.bpl(41,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(43,20): anon4_LoopBody
+Timeouts0.bpl(48,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(31,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(48,5): anon5_LoopDone
+Timeouts0.bpl(50,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(52,11): anon5_LoopBody
+Timeouts0.bpl(70,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(72,20): anon4_LoopBody
+Timeouts0.bpl(77,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(60,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(77,5): anon5_LoopDone
+Timeouts0.bpl(79,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(81,11): anon5_LoopBody
+
+Boogie program verifier finished with 0 verified, 0 errors, 3 time outs
diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index c74e9320..c874a1c1 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -23,3 +23,61 @@ procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int) i := i + 1;
}
}
+
+
+procedure TestTimeouts1(in: [int]int, len: int) returns (out: [int]int);
+ requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
+ requires 0 < len;
+ ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
+
+implementation {:timeLimit 8} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
+{
+ var i : int;
+
+ i := 0;
+ out[i] := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);
+ {
+ out[i + 1] := out[i] + 1;
+ i := i + 1;
+ }
+
+ i := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);
+ {
+ i := i + 1;
+ }
+}
+
+
+procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int);
+ requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
+ requires 0 < len;
+ ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
+
+implementation {:timeLimit 2} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
+{
+ var i : int;
+
+ i := 0;
+ out[i] := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);
+ {
+ out[i + 1] := out[i] + 1;
+ i := i + 1;
+ }
+
+ i := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);
+ {
+ i := i + 1;
+ }
+}
|