diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 21:09:37 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 21:09:37 +0100 |
| commit | acbc945043f81a964f1208f4b9c80c557e854a71 (patch) | |
| tree | 81a74fe265263b50201c772d73108c61f1bbfb22 /Test/snapshots/runtest.snapshot | |
| parent | a532c196a517ffda7dbee44fab491bce06f5f18f (diff) | |
Enable snapshot test. This test is unusual in that it doesn't
use .bpl files in the directory directy on the command line. So
instead will tell lit to look for *.snapshot files and provide
one that runs the commands we want in the right directory.
Diffstat (limited to 'Test/snapshots/runtest.snapshot')
| -rw-r--r-- | Test/snapshots/runtest.snapshot | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot new file mode 100644 index 00000000..6edd51ac --- /dev/null +++ b/Test/snapshots/runtest.snapshot @@ -0,0 +1,2 @@ +// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl > %t +// RUN: %diff %s.expect %t |