diff options
| author |  akashlal <unknown> | 2010-09-18 05:09:45 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-09-18 05:09:45 +0000 |
| commit | dbc59dc5f6dd703720df9815ed83158a351417fe (patch) | |
| tree | 3eaa53ca9f398843cfc3295ea6d896dbd97a48c5 /Test/lazyinline/fooret.bpl | |
| parent | 9a7c232927b5470fbefce15a835626008abb468d (diff) | |
Added test for loop extraction
Diffstat (limited to 'Test/lazyinline/fooret.bpl')
| -rw-r--r-- | Test/lazyinline/fooret.bpl | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/Test/lazyinline/fooret.bpl b/Test/lazyinline/fooret.bpl new file mode 100644 index 00000000..c81baaf1 --- /dev/null +++ b/Test/lazyinline/fooret.bpl @@ -0,0 +1,36 @@ +
+procedure A()
+{
+ var x : int;
+ var y : int;
+ var nondet: bool;
+
+start:
+ x := 0;
+ assume y == 2;
+ goto lh;
+
+lh:
+ goto lab1, lab2;
+
+lab1:
+ assume x < y;
+ x := x + 1;
+ havoc nondet;
+ goto lab3, lab4;
+
+lab3:
+ assume !nondet;
+ goto lh;
+
+lab4:
+ assume nondet;
+ return;
+
+lab2:
+ assume x >= y;
+ assert false;
+
+}
+
+
|