diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/aitest9/VarMapFixpoint.bpl | |
Initial set of files.
Diffstat (limited to 'Test/aitest9/VarMapFixpoint.bpl')
| -rw-r--r-- | Test/aitest9/VarMapFixpoint.bpl | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/Test/aitest9/VarMapFixpoint.bpl b/Test/aitest9/VarMapFixpoint.bpl new file mode 100644 index 00000000..6b53467d --- /dev/null +++ b/Test/aitest9/VarMapFixpoint.bpl @@ -0,0 +1,58 @@ +procedure main()
+{
+ var x: int, y: int, z: int;
+
+ start:
+ x := 2;
+ y := 6;
+ goto LoopHead;
+
+ LoopHead:
+ assert y < 10; // error: the loop body sets y to an arbitrary value
+ goto LoopBody, LoopEnd;
+
+ LoopBody:
+ havoc y;
+ goto LoopHead;
+
+ LoopEnd:
+ return;
+}
+
+procedure SimpleWhile5() returns (returnValue: int)
+{
+ var i: int;
+
+ start:
+ returnValue := 1;
+ havoc i;
+ goto LoopHead;
+
+ LoopHead:
+ goto LoopBody, LoopEnd;
+
+ LoopBody:
+ // here, we would simply like to "assume 1 <= i", but the interval domain doesn't interpret
+ // assume commands, so we start a loop
+ i := 1;
+ goto IncLoopHead;
+
+ IncLoopHead:
+ goto IncI, IncDone;
+
+ IncI:
+ i := i + 1;
+ goto IncLoopHead;
+
+ IncDone:
+ // now we have 1 <= i
+ assert 1 <= i;
+
+ returnValue := returnValue * i;
+ i := i - 1;
+ goto LoopHead;
+
+ LoopEnd:
+ assert returnValue >= 1;
+ return;
+}
|