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