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/bar9.bpl | |
| parent | f9d9312fa9c8e649355183e0c46e95ea6ba6e36c (diff) | |
small fix
added regressions
Diffstat (limited to 'Test/stratifiedinline/bar9.bpl')
| -rw-r--r-- | Test/stratifiedinline/bar9.bpl | 45 |
1 files changed, 45 insertions, 0 deletions
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 |