From f6f1765d810714facbb30fa53c663598d04b8158 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 21:15:02 +0100 Subject: Enabled symdiff lit test. --- Test/symdiff/Answer | 6 +++--- Test/symdiff/foo.bpl | 4 +++- Test/symdiff/foo.bpl.expect | 5 +++++ 3 files changed, 11 insertions(+), 4 deletions(-) create mode 100644 Test/symdiff/foo.bpl.expect (limited to 'Test') diff --git a/Test/symdiff/Answer b/Test/symdiff/Answer index ad21a1ea..322dacfd 100644 --- a/Test/symdiff/Answer +++ b/Test/symdiff/Answer @@ -1,5 +1,5 @@ -foo.bpl(15,3): Error BP5001: This assertion might not hold. -foo.bpl(15,3): Error BP5001: This assertion might not hold. -foo.bpl(15,3): Error BP5001: This assertion might not hold. +foo.bpl(17,3): Error BP5001: This assertion might not hold. +foo.bpl(17,3): Error BP5001: This assertion might not hold. +foo.bpl(17,3): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/symdiff/foo.bpl b/Test/symdiff/foo.bpl index 2859aa45..f2c71b8f 100644 --- a/Test/symdiff/foo.bpl +++ b/Test/symdiff/foo.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -z3multipleErrors -errorTrace:0 %s > %t +// RUN: %diff %s.expect %t procedure Foo(x:int) { var ok:bool; @@ -14,4 +16,4 @@ procedure Foo(x:int) assert ok; -} \ No newline at end of file +} diff --git a/Test/symdiff/foo.bpl.expect b/Test/symdiff/foo.bpl.expect new file mode 100644 index 00000000..eec83421 --- /dev/null +++ b/Test/symdiff/foo.bpl.expect @@ -0,0 +1,5 @@ +foo.bpl(17,3): Error BP5001: This assertion might not hold. +foo.bpl(17,3): Error BP5001: This assertion might not hold. +foo.bpl(17,3): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 3 errors -- cgit v1.2.3