summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Shaz Qadeer <qadeer@microsoft.com>2015-10-01 17:35:38 -0700
committerGravatar Shaz Qadeer <qadeer@microsoft.com>2015-10-01 17:35:38 -0700
commitf1b965f1ea91b9512b290a45a12b9578d3843d8c (patch)
tree4097d190752a646c34ece0ae59ac0d55e149baa2
parent0569be4268fe9c6174ff14cd0e9ab1a8170cfd21 (diff)
parentf1d7e9e90e69854f8f33c474f544855abb8508c2 (diff)
Merge branch 'master' of https://github.com/boogie-org/boogie
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs49
1 files changed, 42 insertions, 7 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 4ab0a9c5..9623139a 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -135,7 +135,7 @@ namespace Microsoft.Boogie
foreach (var e in errorInfo.Aux)
{
- if (!(skipExecutionTrace && e.Category.Contains("Execution trace")))
+ if (!(skipExecutionTrace && e.Category != null && e.Category.Contains("Execution trace")))
{
ReportBplError(e.Tok, e.FullMsg, false, tw);
}
@@ -1472,37 +1472,67 @@ namespace Microsoft.Boogie
case VCGen.Outcome.ReachedBound:
tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
break;
+ case VCGen.Outcome.Errors:
case VCGen.Outcome.TimedOut:
if (implName != null && implTok != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
-
+ if (outcome == ConditionGeneration.Outcome.TimedOut || (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts)))
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification of '{1}' timed out after {0} seconds", 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;
+ if (0 < timedOutAssertions.Count)
+ {
+ errorInfo.Msg += string.Format(" with {0} check(s) that timed out individually", timedOutAssertions.Count);
+ }
foreach (Counterexample error in timedOutAssertions)
{
var callError = error as CallCounterexample;
var returnError = error as ReturnCounterexample;
var assertError = error as AssertCounterexample;
IToken tok = null;
+ string msg = null;
if (callError != null)
{
tok = callError.FailingCall.tok;
+ msg = callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.";
}
else if (returnError != null)
{
tok = returnError.FailingReturn.tok;
+ msg = "A postcondition might not hold on this return path.";
}
else
{
tok = assertError.FailingAssert.tok;
+ if (assertError.FailingAssert is LoopInitAssertCmd)
+ {
+ msg = "This loop invariant might not hold on entry.";
+ }
+ else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
+ {
+ msg = "This loop invariant might not be maintained by the loop.";
+ }
+ else
+ {
+ msg = assertError.FailingAssert.ErrorData as string;
+ if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)
+ {
+ msg = assertError.FailingAssert.ErrorMessage;
+ }
+ if (msg == null)
+ {
+ msg = "This assertion might not hold.";
+ }
+ }
}
- errorInfo.AddAuxInfo(tok, string.Format("unverified assertion due to timeout ({0} of {1})", idx++, timedOutAssertions.Count));
+ errorInfo.AddAuxInfo(tok, msg, "Unverified check due to timeout");
}
}
}
@@ -1531,6 +1561,10 @@ namespace Microsoft.Boogie
er(errorInfo);
}
}
+ else
+ {
+ printer.WriteErrorInformation(errorInfo, tw);
+ }
}
}
@@ -1604,8 +1638,9 @@ namespace Microsoft.Boogie
}
else
{
- Interlocked.Add(ref stats.ErrorCount, errors.Count);
- if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, errors.Count); }
+ int cnt = errors.Where(e => !e.IsAuxiliaryCexForDiagnosingTimeouts).Count();
+ Interlocked.Add(ref stats.ErrorCount, cnt);
+ if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); }
}
break;
}