diff options
| author |  wuestholz <unknown> | 2014-11-03 12:45:42 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-11-03 12:45:42 +0100 |
| commit | 91832a0d858ca6319b737de2e14598509b48f2ae (patch) | |
| tree | 76b20e09ee5fdffdd243b96f797c0a460fe231d3 /Source/VCGeneration | |
| parent | 9a033a6dd23183138116c92a4cae06c4448e4247 (diff) | |
Worked on the verification result caching.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 57 |
1 files changed, 28 insertions, 29 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 9a2a9117..a36e2966 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1546,17 +1546,7 @@ namespace VC { var subsumption = Wlp.Subsumption(ac);
var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;
- if (currentImplementation != null
- && currentImplementation.HasCachedSnapshot
- && checksum != null
- && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
- && !currentImplementation.AnyErrorsInCachedSnapshot
- && currentImplementation.InjectedAssumptionVariables.Count == 1
- && relevantAssumpVars.Count == 1)
- {
- TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
- }
- else if (relevantDoomedAssumpVars.Any())
+ if (relevantDoomedAssumpVars.Any())
{
TraceCachingAction(pc, CachingAction.DoNothingToAssert);
}
@@ -1566,30 +1556,39 @@ namespace VC { && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
&& !currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))
{
- bool isTrue;
- var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
- if (!isTrue && alwaysUseSubsumption)
+ if (!currentImplementation.AnyErrorsInCachedSnapshot
+ && currentImplementation.InjectedAssumptionVariables.Count == 1
+ && relevantAssumpVars.Count == 1)
{
- // Bind the assertion expression to a local variable.
- var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
- var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
- incarnationMap[incarnation] = identExpr;
- ac.IncarnationMap[incarnation] = identExpr;
- passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
- copy = identExpr;
- passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));
TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
}
- else if (isTrue)
+ else
{
- if (alwaysUseSubsumption)
+ bool isTrue;
+ var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
+ if (!isTrue && alwaysUseSubsumption)
+ {
+ // Bind the assertion expression to a local variable.
+ var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
+ var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
+ incarnationMap[incarnation] = identExpr;
+ ac.IncarnationMap[incarnation] = identExpr;
+ passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));
+ copy = identExpr;
+ passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));
+ TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
+ }
+ else if (isTrue)
{
- // Turn it into an assume statement.
- TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
- pc = new AssumeCmd(ac.tok, copy);
- pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+ if (alwaysUseSubsumption)
+ {
+ // Turn it into an assume statement.
+ TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
+ pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+ }
+ dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
}
- dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
}
}
else if (currentImplementation != null
|