diff options
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 8 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 8 | ||||
| -rw-r--r-- | Test/snapshots/Snapshots28.v1.bpl | 2 | ||||
| -rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 11 |
4 files changed, 16 insertions, 13 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 5e021f63..437ee67f 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -942,7 +942,7 @@ namespace Microsoft.Boogie { public static class ChecksumHelper
{
- public static void ComputeChecksums(Cmd cmd, Implementation impl, Dictionary<Variable, Expr> incarnationMap, byte[] currentChecksum = null)
+ public static void ComputeChecksums(Cmd cmd, Implementation impl, ISet<Variable> usedVariables, byte[] currentChecksum = null)
{
if (CommandLineOptions.Clo.VerifySnapshots < 2)
{
@@ -967,7 +967,7 @@ namespace Microsoft.Boogie { {
// TODO(wuestholz): Check with Rustan if this makes sense.
tokTxtWr.Write("havoc ");
- var relevantVars = havocCmd.Vars.Where(v => incarnationMap.ContainsKey(v.Decl)).ToList();
+ var relevantVars = havocCmd.Vars.Where(v => usedVariables.Contains(v.Decl) && !v.Decl.Name.StartsWith("a##post##")).ToList();
relevantVars.Emit(tokTxtWr, true);
tokTxtWr.WriteLine(";");
}
@@ -1013,7 +1013,7 @@ namespace Microsoft.Boogie { {
foreach (var c in stateCmd.Cmds)
{
- ComputeChecksums(c, impl, incarnationMap, currentChecksum);
+ ComputeChecksums(c, impl, usedVariables, currentChecksum);
currentChecksum = c.Checksum;
if (c.SugaredCmdChecksum == null)
{
@@ -1023,7 +1023,7 @@ namespace Microsoft.Boogie { }
else
{
- ComputeChecksums(sugaredCmd.Desugaring, impl, incarnationMap, currentChecksum);
+ ComputeChecksums(sugaredCmd.Desugaring, impl, usedVariables, currentChecksum);
}
}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index dd7e1eac..cbdacfda 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1298,7 +1298,7 @@ namespace VC { Dictionary<Variable, Expr> preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement
- protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, byte[] currentChecksum = null) {
+ protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, VariableCollector variableCollector, byte[] currentChecksum = null) {
Contract.Requires(b != null);
Contract.Requires(incarnationMap != null);
Contract.Requires(mvInfo != null);
@@ -1308,7 +1308,8 @@ namespace VC { List<Cmd> passiveCmds = new List<Cmd>();
foreach (Cmd c in b.Cmds) {
Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction
- ChecksumHelper.ComputeChecksums(c, currentImplementation, incarnationMap, currentChecksum);
+ ChecksumHelper.ComputeChecksums(c, currentImplementation, variableCollector.usedVars, currentChecksum);
+ variableCollector.Visit(c);
currentChecksum = c.Checksum;
TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, b);
}
@@ -1408,6 +1409,7 @@ namespace VC { Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation = new Dictionary<Block, Dictionary<Variable, Expr>>();
Block exitBlock = null;
Dictionary<Variable, Expr> exitIncarnationMap = null;
+ var variableCollector = new VariableCollector();
foreach (Block b in sortedNodes) {
Contract.Assert(b != null);
Contract.Assert(!block2Incarnation.ContainsKey(b));
@@ -1442,7 +1444,7 @@ namespace VC { }
#endregion Each block's map needs to be available to successor blocks
- TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, currentChecksum);
+ TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, variableCollector, currentChecksum);
exitBlock = b;
exitIncarnationMap = incarnationMap;
}
diff --git a/Test/snapshots/Snapshots28.v1.bpl b/Test/snapshots/Snapshots28.v1.bpl index 881fa496..0312b6a6 100644 --- a/Test/snapshots/Snapshots28.v1.bpl +++ b/Test/snapshots/Snapshots28.v1.bpl @@ -12,5 +12,5 @@ implementation {:id "M"} {:checksum "2"} M() }
assert 0 == 0;
- assert x == 0; // TODO(wuestholz): This should fail.
+ assert x == 0;
}
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 3b47d2f3..e2355cd6 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -507,9 +507,10 @@ Processing command (at Snapshots28.v0.bpl(14,5)) assert x == 0 /* checksum: 01-A >>> did nothing
Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0 /* checksum: AB-78-39-B7-C9-1E-4B-24-B5-1A-52-BE-B2-1A-90-D9 */ ;
- >>> turned assertion into assume statement
-Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0 /* checksum: 01-A7-D9-2B-A8-C4-4F-BB-44-22-BE-B6-E1-5F-6E-BF */ ;
- >>> turned assertion into assume statement
+Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0 /* checksum: B7-69-FE-C9-83-D5-67-99-AA-4C-CE-F9-C4-21-A6-3E */ ;
+ >>> did nothing
+Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0 /* checksum: 9D-98-FC-55-22-AD-23-60-39-30-A2-93-D3-86-04-7A */ ;
+ >>> did nothing
+Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 0 verified, 1 error
|