diff options
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 39 | ||||
| -rw-r--r-- | Test/test2/AssertVerifiedUnder0.bpl | 39 | ||||
| -rw-r--r-- | Test/test2/AssertVerifiedUnder0.bpl.expect | 11 |
3 files changed, 74 insertions, 15 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 24c36e3b..6f6326d1 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -109,18 +109,18 @@ namespace VC { ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
VCExprLetBinding LB = null;
- VCExpr A = null;
+ VCExpr VU = null;
if (ac.VerifiedUnder != null)
{
var V = gen.Variable(ctxt.FreshLetBindingName(), Microsoft.Boogie.Type.Bool);
LB = gen.LetBinding(V, C);
C = V;
- A = gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder), V);
+ VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
}
+ VCExpr R = null;
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
- var res = gen.Implies(C, N);
- return A != null ? gen.Let(gen.ImpliesSimp(A, res), LB) : res;
+ R = gen.Implies(C, N);
} else {
int id = ac.UniqueId;
if (ctxt.Label2absy != null) {
@@ -142,30 +142,39 @@ namespace VC { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected case
}
- // (MSchaef) Hack: This line might be useless, but at least it is not harmful
- // need to test it
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- return gen.Implies(C, N);
-
ctxt.AssertionCount++;
+
+ // TODO(wuestholz): Try to weaken the assertion instead of assuming the property that has already been verified:
+ // if (VU != null)
+ // {
+ // C = gen.OrSimp(VU, C);
+ // }
+
if (ctxt.ControlFlowVariableExpr == null) {
Contract.Assert(ctxt.Label2absy != null);
- var res = gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);
- return A != null ? gen.Let(gen.ImpliesSimp(A, res), LB) : res;
+ R = gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);
} else {
VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(ctxt.ControlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId)));
Contract.Assert(controlFlowFunctionAppl != null);
VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(-ac.UniqueId)));
if (ctxt.Label2absy == null) {
- var res = gen.AndSimp(gen.Implies(assertFailure, C), N);
- return A != null ? gen.Let(gen.ImpliesSimp(A, res), LB) : res;
+ R = gen.AndSimp(gen.Implies(assertFailure, C), N);
} else {
- var res = gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), N);
- return A != null ? gen.Let(gen.ImpliesSimp(A, res), LB) : res;
+ R = gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), N);
}
}
}
+ if (VU != null)
+ {
+ R = gen.ImpliesSimp(gen.ImpliesSimp(VU, C), R);
+ }
+
+ if (LB != null)
+ {
+ R = gen.Let(R, LB);
+ }
+ return R;
} else if (cmd is AssumeCmd) {
AssumeCmd ac = (AssumeCmd)cmd;
diff --git a/Test/test2/AssertVerifiedUnder0.bpl b/Test/test2/AssertVerifiedUnder0.bpl new file mode 100644 index 00000000..9e82545f --- /dev/null +++ b/Test/test2/AssertVerifiedUnder0.bpl @@ -0,0 +1,39 @@ +// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure Test0()
+{
+ assert {:verified_under false} false; // error
+}
+
+
+procedure Test1()
+{
+ assert {:verified_under true} false;
+}
+
+
+procedure Test2(P: bool, A: bool)
+{
+ assert {:verified_under A} P; // error
+}
+
+
+procedure Test3(P: bool, A: bool)
+ requires !A ==> P;
+{
+ assert {:verified_under A} P;
+}
+
+
+procedure Test4(P: bool, A: bool)
+{
+ assert {:verified_under A} {:verified_under true} P; // error
+}
+
+
+procedure Test5(P: bool, A: bool)
+ requires !A ==> P;
+{
+ assert {:verified_under A} {:verified_under true} P;
+}
diff --git a/Test/test2/AssertVerifiedUnder0.bpl.expect b/Test/test2/AssertVerifiedUnder0.bpl.expect new file mode 100644 index 00000000..83016c63 --- /dev/null +++ b/Test/test2/AssertVerifiedUnder0.bpl.expect @@ -0,0 +1,11 @@ +AssertVerifiedUnder0.bpl(6,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssertVerifiedUnder0.bpl(6,5): anon0
+AssertVerifiedUnder0.bpl(18,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssertVerifiedUnder0.bpl(18,5): anon0
+AssertVerifiedUnder0.bpl(31,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssertVerifiedUnder0.bpl(31,5): anon0
+
+Boogie program verifier finished with 3 verified, 3 errors
|