summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs37
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs13
-rw-r--r--Source/VCGeneration/VC.cs1
3 files changed, 48 insertions, 3 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 15fdc081..4ab0a9c5 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1459,11 +1459,11 @@ namespace Microsoft.Boogie
printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
- ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
+ ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors);
}
- private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
+ private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List<Counterexample> errors)
{
ErrorInformation errorInfo = null;
@@ -1476,6 +1476,35 @@ namespace Microsoft.Boogie
if (implName != null && implTok != null)
{
errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
+
+ // Report timed out assertions as auxiliary info.
+ if (errors != null)
+ {
+ var cmpr = new CounterexampleComparer();
+ var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList();
+ timedOutAssertions.Sort(cmpr);
+ int idx = 1;
+ foreach (Counterexample error in timedOutAssertions)
+ {
+ var callError = error as CallCounterexample;
+ var returnError = error as ReturnCounterexample;
+ var assertError = error as AssertCounterexample;
+ IToken tok = null;
+ if (callError != null)
+ {
+ tok = callError.FailingCall.tok;
+ }
+ else if (returnError != null)
+ {
+ tok = returnError.FailingReturn.tok;
+ }
+ else
+ {
+ tok = assertError.FailingAssert.tok;
+ }
+ errorInfo.AddAuxInfo(tok, string.Format("unverified assertion due to timeout ({0} of {1})", idx++, timedOutAssertions.Count));
+ }
+ }
}
break;
case VCGen.Outcome.OutOfMemory:
@@ -1592,6 +1621,10 @@ namespace Microsoft.Boogie
errors.Sort(new CounterexampleComparer());
foreach (Counterexample error in errors)
{
+ if (error.IsAuxiliaryCexForDiagnosingTimeouts)
+ {
+ continue;
+ }
var errorInfo = CreateErrorInformation(error, outcome);
errorInfo.ImplementationName = implName;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 1f010757..ae0a1147 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,6 +85,7 @@ namespace Microsoft.Boogie {
public string RequestId;
public abstract byte[] Checksum { get; }
public byte[] SugaredCmdChecksum;
+ public bool IsAuxiliaryCexForDiagnosingTimeouts;
public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
@@ -313,7 +314,7 @@ namespace Microsoft.Boogie {
public abstract int GetLocation();
}
- public class CounterexampleComparer : IComparer<Counterexample> {
+ public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> {
private int Compare(List<Block> bs1, List<Block> bs2)
{
@@ -375,6 +376,16 @@ namespace Microsoft.Boogie {
}
return -1;
}
+
+ public bool Equals(Counterexample x, Counterexample y)
+ {
+ return Compare(x, y) == 0;
+ }
+
+ public int GetHashCode(Counterexample obj)
+ {
+ return 0;
+ }
}
public class AssertCounterexample : Counterexample {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 94584027..33e2f928 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2113,6 +2113,7 @@ namespace VC {
foreach (var cmd in assertCmds)
{
Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);
+ cex.IsAuxiliaryCexForDiagnosingTimeouts = true;
callback.OnCounterexample(cex, msg);
}
}