From edd49fda92881753f149d667d39bba9ad07cbb70 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 10 Dec 2012 12:21:16 +0530 Subject: More stuff for abstract houdini; updated test case --- Test/AbsHoudini/Answer | 18 +++++------------- Test/AbsHoudini/f1.bpl | 6 +++--- 2 files changed, 8 insertions(+), 16 deletions(-) (limited to 'Test/AbsHoudini') diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer index 376d9f3a..d2418bd4 100644 --- a/Test/AbsHoudini/Answer +++ b/Test/AbsHoudini/Answer @@ -1,19 +1,11 @@ -------------------- f1.bpl -------------------- -Running Abstract Houdini - Post: g == old(g) + 1 - Post: g == old(g) + 2 - Post: g == old(g) + 3 - Pre: old(g) == 0 -Trying summary for foo: (And (== (fooSummaryPred g g@0) false) (== (fooSummaryPred g g@0) false)) -Trying summary for foo: (And (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3))))) (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3)))))) -Trying summary for foo: (And (== (fooSummaryPred g g@0) (== g@0 (+ g 1))) (== (fooSummaryPred g g@0) (== g@0 (+ g 1)))) -Trying summary for main: (And (== (mainSummaryPred g g@3) false) (== (mainSummaryPred g g@3) false)) -Trying summary for main: (And (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3))))) (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3)))))) -Trying summary for main: (And (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1)))) (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1))))) -Summary of main: -(old(g) == 0 ==> g == old(g) + 1) Summary of foo: g == old(g) + 1 +Summary of main: +(old(g) == 0 ==> g == old(g) + 1) +Prover time = 0.0260026 +Number of prover queries = 6 +Witness written to absHoudiniWitness.bpl Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl index 5ea6797b..e5ed85ef 100644 --- a/Test/AbsHoudini/f1.bpl +++ b/Test/AbsHoudini/f1.bpl @@ -26,7 +26,7 @@ procedure foo() } procedure {:template} summaryTemplate(); - ensures g == old(g) + 1; - ensures g == old(g) + 2; - ensures g == old(g) + 3; + ensures {:post} g == old(g) + 1; + ensures {:post} g == old(g) + 2; + ensures {:post} g == old(g) + 3; ensures {:pre} old(g) == 0; -- cgit v1.2.3