diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-04 09:34:14 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-04 09:34:14 -0700 |
| commit | 3ff2e42970584ad66f8b8e353ddce86dbea92baf (patch) | |
| tree | b506751550be2b708766fc0eca39edddf6ddb8ef /Test/stratifiedinline | |
| parent | f9d9312fa9c8e649355183e0c46e95ea6ba6e36c (diff) | |
small fix
added regressions
Diffstat (limited to 'Test/stratifiedinline')
| -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 |
6 files changed, 522 insertions, 2 deletions
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 -----
|