diff options
| author |  schaef <unknown> | 2010-10-13 10:07:55 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2010-10-13 10:07:55 +0000 |
| commit | e21b147ddbaf49bf6cc44df2046d3af4235622c9 (patch) | |
| tree | 2de4e585dc50437f8c3bef2b65910e937820af6a /Test/doomed | |
| parent | 540a44898edd1587063b7ce6b15a588bb272bc28 (diff) | |
Bug fixes and speed up for doomed program point analysis
Diffstat (limited to 'Test/doomed')
| -rw-r--r-- | Test/doomed/doomed.bpl | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl index 741a54c5..9029383d 100644 --- a/Test/doomed/doomed.bpl +++ b/Test/doomed/doomed.bpl @@ -36,6 +36,22 @@ procedure evilloop(x:int) }
}
+procedure evilnested(x:int)
+{
+ var i : int;
+ var j : int;
+ i:=x-1;
+ j:=1;
+ while (i>=0) {
+ while (j<=i) {
+ assert j<x;
+ j := j+1;
+ }
+ i := i - 1;
+ }
+}
+
+
procedure evilpath(x:int)
{
var y : int;
|