From e4164dd5c959a5252a0954f980bb900581286707 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 21 Sep 2014 22:17:25 +0100 Subject: Add missing run lines (based off Test/doomed/runtest.bat) to doomed tests. These are really broken because Boogie just seems to hang when they are executed. So they aren't executed right now. I'm not sure what to do with the other .bpl files. ``schaef`` left them lying around. --- Test/doomed/doomed.bpl | 2 +- Test/doomed/notdoomed.bpl | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'Test/doomed') diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl index 9029383d..9dea47b7 100644 --- a/Test/doomed/doomed.bpl +++ b/Test/doomed/doomed.bpl @@ -1,4 +1,4 @@ - +// RUN: %boogie -vc:doomed %s procedure evilrequires(x:int) requires x>0; { diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl index c3193a01..8d57db71 100644 --- a/Test/doomed/notdoomed.bpl +++ b/Test/doomed/notdoomed.bpl @@ -1,3 +1,4 @@ +// RUN: %boogie -vc:doomed %s procedure a(x:int) { var y : int; -- cgit v1.2.3