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 | |
| parent | 5e52d81030d85b76cc6a0209617af8c21159755d (diff) | |
Worked on the more advanced verification result caching.
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 6 | ||||
| -rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 4 |
3 files changed, 6 insertions, 10 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);
}
}
}
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 80325bea..90c1c90b 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -127,14 +127,14 @@ Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error
Snapshots20.v1.bpl(9,9): Error BP5001: This assertion might not hold.
-Snapshots20.v1.bpl(13,9): Error BP5001: This assertion might not hold.
+Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
Boogie program verifier finished with 0 verified, 2 errors
Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.
Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
Boogie program verifier finished with 0 verified, 2 errors
-Snapshots21.v1.bpl(11,9): Error BP5001: This assertion might not hold.
+Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.
Boogie program verifier finished with 0 verified, 2 errors
|