summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-07-10 10:25:53 +0200
committerGravatar wuestholz <unknown>2014-07-10 10:25:53 +0200
commite721ac469b8aa3f964ad24917757168288826da1 (patch)
treee9c1d877f54fa7000ff96bbcb90c5b79c1d63003 /Source/VCGeneration/ConditionGeneration.cs
parent736eb8d7b2d80e7672fcdffba8d731c7bb9bb9d7 (diff)
Worked on the more advanced verification result caching.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs14
1 files changed, 12 insertions, 2 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index cdeb6c2c..25ddc2c0 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1531,14 +1531,24 @@ namespace VC {
passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));
}
else if (currentImplementation != null
+ && ac.Checksum != null
+ && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
+ && currentImplementation.ErrorChecksumToCachedError != null
+ && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
+ && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
+ {
+ // Turn it into an assume statement.
+ // TODO(wuestholz): Uncomment this.
+ // pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+ }
+ else if (currentImplementation != null
&& currentImplementation.AnyErrorsInCachedSnapshot
&& ac.Checksum != null
&& (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
&& currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
&& (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
{
- // TODO(wuestholz): Do the same for assertions if they have been proved in the previous snapshot.
-
// Turn it into an assume statement.
// TODO(wuestholz): Uncomment this.
// pc = new AssumeCmd(ac.tok, copy);