diff options
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 12 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 21 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 3 |
3 files changed, 20 insertions, 16 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 2b16651b..61d8cdc4 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -984,6 +984,7 @@ namespace Microsoft.Boogie { // because a corresponding counterexample will also have the
// checksum of the failing call.
impl.AddAssertionChecksum(assertRequiresCmd.Call.Checksum);
+ assertRequiresCmd.SugaredCmdChecksum = assertRequiresCmd.Call.Checksum;
}
else
{
@@ -1002,13 +1003,15 @@ namespace Microsoft.Boogie { {
ComputeChecksums(c, impl, currentChecksum);
currentChecksum = c.Checksum;
+ if (c.SugaredCmdChecksum == null)
+ {
+ c.SugaredCmdChecksum = cmd.Checksum;
+ }
}
- sugaredCmd.DesugaringChecksum = currentChecksum;
}
else
{
ComputeChecksums(sugaredCmd.Desugaring, impl, currentChecksum);
- sugaredCmd.DesugaringChecksum = sugaredCmd.Desugaring.Checksum;
}
}
}
@@ -1036,6 +1039,7 @@ namespace Microsoft.Boogie { [ContractClass(typeof(CmdContracts))]
public abstract class Cmd : Absy {
public byte[] Checksum { get; internal set; }
+ public byte[] SugaredCmdChecksum { get; internal set; }
public Cmd(IToken/*!*/ tok)
: base(tok) {
@@ -1760,9 +1764,7 @@ namespace Microsoft.Boogie { [ContractClass(typeof(SugaredCmdContracts))]
abstract public class SugaredCmd : Cmd {
private Cmd desugaring; // null until desugared
-
- public byte[] DesugaringChecksum { get; set; }
-
+
public SugaredCmd(IToken/*!*/ tok)
: base(tok) {
Contract.Requires(tok != null);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 98f0110a..7fb12589 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1491,6 +1491,7 @@ namespace VC { var dropCmd = false;
var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();
var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();
+ var checksum = pc.SugaredCmdChecksum != null ? pc.SugaredCmdChecksum : pc.Checksum;
if (pc is AssertCmd) {
var ac = (AssertCmd)pc;
ac.OrigExpr = ac.Expr;
@@ -1508,9 +1509,9 @@ namespace VC { { }
else if (currentImplementation != null
&& currentImplementation.HasCachedSnapshot
- && ac.Checksum != null
- && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)
- && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))
+ && checksum != null
+ && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
+ && !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
{
bool isTrue;
var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
@@ -1539,9 +1540,9 @@ namespace VC { else if (currentImplementation != null
&& currentImplementation.HasCachedSnapshot
&& relevantAssumpVars.Count == 0
- && ac.Checksum != null
- && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)
- && currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))
+ && checksum != null
+ && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
+ && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
{
if (alwaysUseSubsumption)
{
@@ -1557,13 +1558,13 @@ namespace VC { }
}
else if (pc is AssumeCmd
- && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot"))
+ && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")
+ && pc.SugaredCmdChecksum != null)
{
if (!relevantDoomedAssumpVars.Any()
&& currentImplementation.HasCachedSnapshot
- && pc.Checksum != null
- && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.Checksum)
- && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.Checksum))
+ && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.SugaredCmdChecksum)
+ && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.SugaredCmdChecksum))
{
bool isTrue;
var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 6a039923..d92f8661 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1626,7 +1626,8 @@ namespace VC { outcome = Outcome.Errors;
foreach (var a in impl.RecycledFailingAssertions)
{
- var oldCex = impl.ErrorChecksumToCachedError[a.Checksum] as Counterexample;
+ var checksum = a.SugaredCmdChecksum != null ? a.SugaredCmdChecksum : a.Checksum;
+ var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;
if (oldCex != null)
{
callback.OnCounterexample(oldCex, null);
|