diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-08-24 01:16:59 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-08-24 01:16:59 +0530 |
| commit | 64b57a073afe03ab57d99c96ef6994b77f786d0e (patch) | |
| tree | c30b495975bcd0c0299b864945408525b92332f0 /Test/extractloops/t3.bpl | |
| parent | 426914e83193a9434a360d0d0ca4752fdf752e64 (diff) | |
Support for irreducible graphs (with extractLoops)
Diffstat (limited to 'Test/extractloops/t3.bpl')
| -rw-r--r-- | Test/extractloops/t3.bpl | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl new file mode 100644 index 00000000..e5fad6d1 --- /dev/null +++ b/Test/extractloops/t3.bpl @@ -0,0 +1,42 @@ +var g: int;
+
+procedure A();
+ requires g == 0;
+ modifies g;
+
+procedure {:inline 1} {:verify false} foo();
+
+implementation foo() {
+ var t: int;
+ t := 0;
+}
+
+implementation A()
+{
+ var x: int;
+ var y: int;
+
+ anon0:
+ x := 4;
+ goto anon3_LoopHead, anon3_LoopBody;
+
+ anon3_LoopHead:
+ call foo();
+ goto anon3_LoopDone, anon3_LoopBody;
+
+ anon3_LoopBody:
+ assume g < x;
+ g := g + 1;
+ x := x - 1;
+ goto anon3_LoopHead;
+
+ anon3_LoopDone:
+ assume g >= x;
+ goto anon2;
+
+ anon2:
+ assert x == 1;
+ return;
+}
+
+
|