diff options
| author |  wuestholz <unknown> | 2014-07-10 10:25:53 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-07-10 10:25:53 +0200 |
| commit | e721ac469b8aa3f964ad24917757168288826da1 (patch) | |
| tree | e9c1d877f54fa7000ff96bbcb90c5b79c1d63003 /Source/VCGeneration/ConditionGeneration.cs | |
| parent | 736eb8d7b2d80e7672fcdffba8d731c7bb9bb9d7 (diff) | |
Worked on the more advanced verification result caching.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 14 |
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);
|