From 67a0a458aad9ece669a49cca085b695a56003d0e Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 16 Nov 2015 12:50:24 -0600 Subject: Add a test. --- Test/test1/StatementIds0.bpl | 15 ++++++++++++--- Test/test1/StatementIds0.bpl.expect | 4 +++- 2 files changed, 15 insertions(+), 4 deletions(-) (limited to 'Test') diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl index 85b9cd36..abf26159 100644 --- a/Test/test1/StatementIds0.bpl +++ b/Test/test1/StatementIds0.bpl @@ -3,13 +3,22 @@ procedure test0(n: int) { - assume {:id "s0"} 0 < n; - assert {:id "s0"} 0 < n; + assume {:id "s0"} true; + assert {:id "s0"} true; } -procedure test1(n: int) +procedure test1() { call {:id "s0"} P(); } +procedure test2(n: int) +{ + while (*) + invariant {:id "s0"} true; + invariant {:id "s0"} true; + { + } +} + procedure P(); diff --git a/Test/test1/StatementIds0.bpl.expect b/Test/test1/StatementIds0.bpl.expect index 944c3257..4783d912 100644 --- a/Test/test1/StatementIds0.bpl.expect +++ b/Test/test1/StatementIds0.bpl.expect @@ -1,3 +1,5 @@ StatementIds0.bpl(7,4): Error: more than one statement with same id: s0 StatementIds0.bpl(12,4): Error: more than one statement with same id: s0 -2 name resolution errors detected in StatementIds0.bpl +StatementIds0.bpl(18,6): Error: more than one statement with same id: s0 +StatementIds0.bpl(19,6): Error: more than one statement with same id: s0 +4 name resolution errors detected in StatementIds0.bpl -- cgit v1.2.3