diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/aitest9/TestIntervals.bpl | 16 | ||||
| -rw-r--r-- | Test/aitest9/answer | 2 | ||||
| -rw-r--r-- | Test/stratifiedinline/Answer | 422 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar10.bpl | 41 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar7.bpl | 2 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar8.bpl | 2 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar9.bpl | 45 | ||||
| -rw-r--r-- | Test/stratifiedinline/runtest.bat | 12 |
8 files changed, 539 insertions, 3 deletions
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index b989e16c..bee73a57 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -22,3 +22,19 @@ procedure P() assert -3 <= c;
assert c <= 0; // error (there was once an error in the Intervals which thought this assertion to be true)
}
+
+// The following tests a triply nested array, where the innermost array is a polymorphic map.
+// There was once an error in Boogie's handling of such things in the AI code.
+
+type ref;
+type teflon;
+
+type Field a;
+type HeapType = <a>[Field a]a;
+var Heap: HeapType;
+
+procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon)
+ modifies Heap;
+{
+ Heap[myField][r][t] := true;
+}
diff --git a/Test/aitest9/answer b/Test/aitest9/answer index 27e18ca4..d68508af 100644 --- a/Test/aitest9/answer +++ b/Test/aitest9/answer @@ -18,4 +18,4 @@ Execution trace: TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
-Boogie program verifier finished with 0 verified, 1 error
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aee2722e..6e23c098 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -62,3 +62,425 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test bar7.bpl
+bar7.bpl(42,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar7.bpl(35,5): anon0
+ bar7.bpl(37,5): anon4_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ bar7.bpl(42,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar8.bpl
+bar8.bpl(41,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar8.bpl(34,5): anon0
+ bar8.bpl(36,5): anon4_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ bar8.bpl(41,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar9.bpl
+bar9.bpl(44,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar9.bpl(35,5): anon0
+ bar9.bpl(41,5): anon4_Else
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(16,3): anon2_Else
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(26,3): anon2_Else
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ bar9.bpl(44,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar10.bpl
+bar10.bpl(40,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar10.bpl(35,5): anon0
+ Inlined call to procedure bar1 begins
+ bar10.bpl(16,3): anon0
+ bar10.bpl(16,3): anon2_Else
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar2 begins
+ bar10.bpl(26,3): anon0
+ bar10.bpl(26,3): anon2_Else
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl new file mode 100644 index 00000000..8cfcfc13 --- /dev/null +++ b/Test/stratifiedinline/bar10.bpl @@ -0,0 +1,41 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+ if (i < 20) {
+ i := i + 1;
+ call foo();
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ call bar1(0);
+ call bar2(0);
+ i := 0;
+ call foo();
+ assert i < 10;
+}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index 747510de..b28777bd 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo()
modifies i;
{
- if (i < 80) {
+ if (i < 20) {
i := i + 1;
call foo();
}
diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index d447e3a7..e96655f3 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo()
modifies i;
{
- if (i < 80) {
+ if (i < 20) {
i := i + 1;
call foo();
}
diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl new file mode 100644 index 00000000..12de78ad --- /dev/null +++ b/Test/stratifiedinline/bar9.bpl @@ -0,0 +1,45 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo(x: int)
+modifies i;
+{
+ if (i < x) {
+ i := i + 1;
+ call foo(x);
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ if (*) {
+ call foo(20);
+ i := 0;
+ call foo(4);
+ } else {
+ call bar1(0);
+ call bar2(0);
+ }
+ assert i < 10;
+}
\ No newline at end of file diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index 194570d0..d731d605 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -19,4 +19,16 @@ echo ----- echo ----- Running regression test bar6.bpl
%BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl
echo -----
+echo ----- Running regression test bar7.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar7.bpl
+echo -----
+echo ----- Running regression test bar8.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar8.bpl
+echo -----
+echo ----- Running regression test bar9.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar9.bpl
+echo -----
+echo ----- Running regression test bar10.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl
+echo -----
|