diff options
| author |  wuestholz <unknown> | 2014-07-10 13:47:44 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-07-10 13:47:44 +0200 |
| commit | 9abbf5e9060e152fb13c0cd5c9fbbdc3aba19f30 (patch) | |
| tree | dd4ee649076e5b1a0db2cdc40542554a7f54be22 /Source | |
| parent | 5e52d81030d85b76cc6a0209617af8c21159755d (diff) | |
Worked on the more advanced verification result caching.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 6 |
2 files changed, 4 insertions, 8 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 25ddc2c0..5304a789 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1538,8 +1538,7 @@ namespace VC { && (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 = new AssumeCmd(ac.tok, copy);
pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
}
else if (currentImplementation != null
@@ -1550,8 +1549,7 @@ namespace VC { && (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 = new AssumeCmd(ac.tok, copy);
pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
currentImplementation.AddRecycledFailingAssertion(ac);
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 239cecdb..18e47ac1 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1623,15 +1623,13 @@ namespace VC { // Report all recycled failing assertions for this implementation.
if (impl.RecycledFailingAssertions != null && impl.RecycledFailingAssertions.Any())
{
- // TODO(wuestholz): Uncomment this.
- // outcome = Outcome.Errors;
+ outcome = Outcome.Errors;
foreach (var a in impl.RecycledFailingAssertions)
{
var oldCex = impl.ErrorChecksumToCachedError[a.Checksum] as Counterexample;
if (oldCex != null)
{
- // TODO(wuestholz): Uncomment this.
- // callback.OnCounterexample(oldCex, null);
+ callback.OnCounterexample(oldCex, null);
}
}
}
|