From 95d752d7480ecddb727df1cc3613fefa4363b960 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 19:04:59 +0100 Subject: Enable "abstract domain of intervals" lit tests. --- Test/aitest9/TestIntervals.bpl | 2 ++ Test/aitest9/TestIntervals.bpl.expect | 20 ++++++++++++++++++ Test/aitest9/VarMapFixpoint.bpl | 2 ++ Test/aitest9/VarMapFixpoint.bpl.expect | 7 +++++++ Test/aitest9/answer | 38 +++++++++++++++++----------------- 5 files changed, 50 insertions(+), 19 deletions(-) create mode 100644 Test/aitest9/TestIntervals.bpl.expect create mode 100644 Test/aitest9/VarMapFixpoint.bpl.expect (limited to 'Test/aitest9') diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index 622a0b36..6d968bc9 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s -infer:j > %t +// RUN: %diff %s.expect %t procedure P() { var a: int, b: int, c: int; diff --git a/Test/aitest9/TestIntervals.bpl.expect b/Test/aitest9/TestIntervals.bpl.expect new file mode 100644 index 00000000..b4b7175e --- /dev/null +++ b/Test/aitest9/TestIntervals.bpl.expect @@ -0,0 +1,20 @@ +TestIntervals.bpl(25,3): Error BP5001: This assertion might not hold. +Execution trace: + TestIntervals.bpl(7,5): anon0 + TestIntervals.bpl(8,3): anon9_LoopHead + TestIntervals.bpl(14,14): anon10_Then + TestIntervals.bpl(15,14): anon11_Then + TestIntervals.bpl(16,14): anon12_Then + TestIntervals.bpl(19,5): anon8 +TestIntervals.bpl(70,3): Error BP5001: This assertion might not hold. +Execution trace: + TestIntervals.bpl(62,3): anon0 + TestIntervals.bpl(67,3): anon3_LoopHead + TestIntervals.bpl(67,3): anon3_LoopDone +TestIntervals.bpl(71,3): Error BP5001: This assertion might not hold. +Execution trace: + TestIntervals.bpl(62,3): anon0 + TestIntervals.bpl(67,3): anon3_LoopHead + TestIntervals.bpl(67,3): anon3_LoopDone + +Boogie program verifier finished with 2 verified, 3 errors diff --git a/Test/aitest9/VarMapFixpoint.bpl b/Test/aitest9/VarMapFixpoint.bpl index 6b53467d..1ee8d694 100644 --- a/Test/aitest9/VarMapFixpoint.bpl +++ b/Test/aitest9/VarMapFixpoint.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s -infer:j > %t +// RUN: %diff %s.expect %t procedure main() { var x: int, y: int, z: int; diff --git a/Test/aitest9/VarMapFixpoint.bpl.expect b/Test/aitest9/VarMapFixpoint.bpl.expect new file mode 100644 index 00000000..7037f324 --- /dev/null +++ b/Test/aitest9/VarMapFixpoint.bpl.expect @@ -0,0 +1,7 @@ +VarMapFixpoint.bpl(13,5): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + VarMapFixpoint.bpl(7,3): start + VarMapFixpoint.bpl(12,3): LoopHead + VarMapFixpoint.bpl(16,3): LoopBody + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/aitest9/answer b/Test/aitest9/answer index 88af771c..ef9f4d83 100644 --- a/Test/aitest9/answer +++ b/Test/aitest9/answer @@ -1,31 +1,31 @@ -------------------- VarMapFixPoint.bpl -------------------- -VarMapFixPoint.bpl(11,5): Error BP5005: This loop invariant might not be maintained by the loop. +VarMapFixPoint.bpl(13,5): Error BP5005: This loop invariant might not be maintained by the loop. Execution trace: - VarMapFixPoint.bpl(5,3): start - VarMapFixPoint.bpl(10,3): LoopHead - VarMapFixPoint.bpl(14,3): LoopBody + VarMapFixPoint.bpl(7,3): start + VarMapFixPoint.bpl(12,3): LoopHead + VarMapFixPoint.bpl(16,3): LoopBody Boogie program verifier finished with 1 verified, 1 error -------------------- TestIntervals.bpl -------------------- -TestIntervals.bpl(23,3): Error BP5001: This assertion might not hold. +TestIntervals.bpl(25,3): Error BP5001: This assertion might not hold. Execution trace: - TestIntervals.bpl(5,5): anon0 - TestIntervals.bpl(6,3): anon9_LoopHead - TestIntervals.bpl(12,14): anon10_Then - TestIntervals.bpl(13,14): anon11_Then - TestIntervals.bpl(14,14): anon12_Then - TestIntervals.bpl(17,5): anon8 -TestIntervals.bpl(68,3): Error BP5001: This assertion might not hold. + TestIntervals.bpl(7,5): anon0 + TestIntervals.bpl(8,3): anon9_LoopHead + TestIntervals.bpl(14,14): anon10_Then + TestIntervals.bpl(15,14): anon11_Then + TestIntervals.bpl(16,14): anon12_Then + TestIntervals.bpl(19,5): anon8 +TestIntervals.bpl(70,3): Error BP5001: This assertion might not hold. Execution trace: - TestIntervals.bpl(60,3): anon0 - TestIntervals.bpl(65,3): anon3_LoopHead - TestIntervals.bpl(65,3): anon3_LoopDone -TestIntervals.bpl(69,3): Error BP5001: This assertion might not hold. + TestIntervals.bpl(62,3): anon0 + TestIntervals.bpl(67,3): anon3_LoopHead + TestIntervals.bpl(67,3): anon3_LoopDone +TestIntervals.bpl(71,3): Error BP5001: This assertion might not hold. Execution trace: - TestIntervals.bpl(60,3): anon0 - TestIntervals.bpl(65,3): anon3_LoopHead - TestIntervals.bpl(65,3): anon3_LoopDone + TestIntervals.bpl(62,3): anon0 + TestIntervals.bpl(67,3): anon3_LoopHead + TestIntervals.bpl(67,3): anon3_LoopDone Boogie program verifier finished with 2 verified, 3 errors -- cgit v1.2.3