diff options
author | qadeer <unknown> | 2010-08-11 17:16:29 +0000 |
---|---|---|
committer | qadeer <unknown> | 2010-08-11 17:16:29 +0000 |
commit | 97b315c477bdf4e14c15d16e38f13ec08b3a46d6 (patch) | |
tree | edcb11e613927b66ba5964a6b4d352659f082709 /Test/lazyinline/foo.bpl | |
parent | 78ee8223d2bab10b38f3e42c450126d6171e4536 (diff) |
Added the option /extractLoops to extract loops as procedure calls. If either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
Diffstat (limited to 'Test/lazyinline/foo.bpl')
-rw-r--r-- | Test/lazyinline/foo.bpl | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Test/lazyinline/foo.bpl b/Test/lazyinline/foo.bpl new file mode 100644 index 00000000..80b7b7b2 --- /dev/null +++ b/Test/lazyinline/foo.bpl @@ -0,0 +1,15 @@ +var g: int;
+
+procedure A()
+requires g == 0;
+modifies g;
+ensures g == 2;
+{
+ var x : int;
+ x := 4;
+ while (g < x) {
+ g := g + 1;
+ x := x - 1;
+ }
+ assert x == 2;
+}
\ No newline at end of file |