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/lazyinline/bar5.bpl | |
| parent | ddd16cd53910f044fd4700463ff977091b983897 (diff) | |
added reachability information to the VC and used that to support arbitrary asserts in lazy inlining
Diffstat (limited to 'Test/lazyinline/bar5.bpl')
| -rw-r--r-- | Test/lazyinline/bar5.bpl | 26 |
1 files changed, 26 insertions, 0 deletions
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();
+}
+
|