diff options
| author |  Unknown <qadeer@Shakespeare.redmond.corp.microsoft.com> | 2011-04-14 22:34:06 -0700 |
|---|---|---|
| committer | Unknown <qadeer@Shakespeare.redmond.corp.microsoft.com> | 2011-04-14 22:34:06 -0700 |
| commit | 6e683025dbc6b7b6f74ed9415178f6f4abff2a24 (patch) | |
| tree | f4eb2a9add18fe78600f6d3a32f3d20c6067ebb4 /Test | |
| parent | ddd16cd53910f044fd4700463ff977091b983897 (diff) | |
added reachability information to the VC and used that to support arbitrary asserts in lazy inlining
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/lazyinline/Answer | 90 | ||||
| -rw-r--r-- | Test/lazyinline/bar5.bpl | 26 | ||||
| -rw-r--r-- | Test/lazyinline/bar7.bpl | 27 | ||||
| -rw-r--r-- | Test/lazyinline/bar8.bpl | 16 | ||||
| -rw-r--r-- | Test/lazyinline/runtest.bat | 9 |
5 files changed, 135 insertions, 33 deletions
diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer index 1feac694..eb3baae3 100644 --- a/Test/lazyinline/Answer +++ b/Test/lazyinline/Answer @@ -2,31 +2,31 @@ bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
- bar1.bpl(24,3): anon0
- Inlined call to procedure foo begins
- bar1.bpl(13,5): anon0
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
+ bar1.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar1.bpl(13,5): anon0
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar2.bpl
bar2.bpl(21,3): Error BP5001: This assertion might not hold.
Execution trace:
- bar2.bpl(19,3): anon0
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(6,7): anon3_Then
- Inlined call to procedure foo ends
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(9,7): anon3_Else
- Inlined call to procedure foo ends
+ bar2.bpl(19,3): anon0
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(6,7): anon3_Then
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(9,7): anon3_Else
+ Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
@@ -34,23 +34,23 @@ Boogie program verifier finished with 0 verified, 1 error bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
- bar3.bpl(38,3): anon0
- Inlined call to procedure foo begins
- bar3.bpl(18,3): anon0
- bar3.bpl(19,7): anon3_Then
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
+ bar3.bpl(38,3): anon0
+ Inlined call to procedure foo begins
+ bar3.bpl(18,3): anon0
+ bar3.bpl(19,7): anon3_Then
Inlined call to procedure bar begins
bar3.bpl(7,3): anon0
- bar3.bpl(10,7): anon3_Else
+ bar3.bpl(8,7): anon3_Then
Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(8,7): anon3_Then
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
Boogie program verifier finished with 0 verified, 1 error
-----
@@ -58,10 +58,34 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test bar5.bpl
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar5.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar5.bpl(13,5): anon0
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
----- Running regression test bar6.bpl
Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test bar7.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
+----- Running regression test bar8.bpl
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar8.bpl(13,5): anon0
+ Inlined call to procedure foo begins
+ bar8.bpl(6,3): anon0
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
----- Running regression test foo.bpl
Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/lazyinline/bar5.bpl b/Test/lazyinline/bar5.bpl new file mode 100644 index 00000000..ec399b4a --- /dev/null +++ b/Test/lazyinline/bar5.bpl @@ -0,0 +1,26 @@ +var x: int;
+var y: int;
+
+procedure {:inline 1} bar()
+modifies y;
+{
+ y := y + 1;
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ x := x + 1;
+ assert x == y;
+ call bar();
+ call bar();
+ x := x + 1;
+}
+
+procedure main()
+requires x == y;
+modifies x, y;
+{
+ call foo();
+}
+
diff --git a/Test/lazyinline/bar7.bpl b/Test/lazyinline/bar7.bpl new file mode 100644 index 00000000..0eff6a7d --- /dev/null +++ b/Test/lazyinline/bar7.bpl @@ -0,0 +1,27 @@ +var x: int;
+var y: int;
+
+procedure {:inline 1} bar()
+modifies y;
+{
+ y := y + 1;
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ x := x + 1;
+ assert x != y;
+ call bar();
+ call bar();
+ x := x + 1;
+ assert x == y;
+}
+
+procedure main()
+requires x == y;
+modifies x, y;
+{
+ call foo();
+}
+
diff --git a/Test/lazyinline/bar8.bpl b/Test/lazyinline/bar8.bpl new file mode 100644 index 00000000..dd6dab31 --- /dev/null +++ b/Test/lazyinline/bar8.bpl @@ -0,0 +1,16 @@ +var x: int;
+var y: int;
+
+procedure {:inline 1} foo()
+{
+ assert x == y;
+}
+
+procedure main()
+requires x == y;
+modifies x, y;
+{
+ x := x + 1;
+ call foo();
+}
+
diff --git a/Test/lazyinline/runtest.bat b/Test/lazyinline/runtest.bat index 6cf0ee1b..e7e86446 100644 --- a/Test/lazyinline/runtest.bat +++ b/Test/lazyinline/runtest.bat @@ -16,9 +16,18 @@ echo ----- echo ----- Running regression test bar4.bpl
%BGEXE% %* /noinfer /lazyInline:1 bar4.bpl
echo -----
+echo ----- Running regression test bar5.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar5.bpl
+echo -----
echo ----- Running regression test bar6.bpl
%BGEXE% %* /noinfer /lazyInline:1 bar6.bpl
echo -----
+echo ----- Running regression test bar7.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar7.bpl
+echo -----
+echo ----- Running regression test bar8.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar8.bpl
+echo -----
echo ----- Running regression test foo.bpl
%BGEXE% %* /noinfer /lazyInline:1 /extractLoops foo.bpl
echo -----
|