From c09814e1ae44a0bee53abb6e8e65b79c1da03d9e Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 6 May 2015 17:52:52 +0200 Subject: Make it preserve the fact that the value of an assumption variable never becomes logically weaker after a havoc. --- Source/VCGeneration/ConditionGeneration.cs | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 515ec16d..206e0ee7 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1742,8 +1742,8 @@ namespace VC { Contract.Assert(c != null); // If an assumption variable for postconditions is included here, it must have been assigned within a loop. // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop - // invariant) in the previous snapshot and are therefore not going refer to the assumption variable after - // the loop. We can achieve this by simply not updating/adding it in the incarnation map. + // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the + // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map. List havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##post##"))).ToList(); // First, compute the new incarnations foreach (IdentifierExpr ie in havocVars) { @@ -1767,6 +1767,18 @@ namespace VC { } } } + + // Add the following assume-statement for each assumption variable 'v', where 'v_post' is the new incarnation and 'v_pre' is the old one: + // assume v_post ==> v_pre; + foreach (IdentifierExpr ie in havocVars) + { + if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption")) + { + var preInc = (Expr)(preHavocIncarnationMap[ie.Decl].Clone()); + var postInc = (Expr)(incarnationMap[ie.Decl].Clone()); + passiveCmds.Add(new AssumeCmd(c.tok, Expr.Imp(postInc, preInc))); + } + } } #endregion else if (c is CommentCmd) { -- cgit v1.2.3