diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-21 22:17:25 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-21 22:17:25 +0100 |
| commit | e4164dd5c959a5252a0954f980bb900581286707 (patch) | |
| tree | 26403dafd8509fc519e58f2aebdb4a551724797d /Test/doomed | |
| parent | 48dbb157f0214610594ef9a67bcea113fd293c57 (diff) | |
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.
Diffstat (limited to 'Test/doomed')
| -rw-r--r-- | Test/doomed/doomed.bpl | 2 | ||||
| -rw-r--r-- | Test/doomed/notdoomed.bpl | 1 |
2 files changed, 2 insertions, 1 deletions
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;
|