diff options
| author |  Rustan Leino <leino@microsoft.com> | 2015-08-27 20:10:41 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2015-08-28 13:29:56 -0700 |
| commit | 21f1cfff139759d9b9f91ed800da2158daca8ed4 (patch) | |
| tree | e9665d1ed7561e244372f167fcc6d90abd32127b /Source/ExecutionEngine/ExecutionEngine.cs | |
| parent | 8f64d5c104efe69c5d561c1b22c3e1320bba04fa (diff) | |
Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code.
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 45 |
1 files changed, 19 insertions, 26 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 67ce49a5..a408642a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -151,25 +151,18 @@ namespace Microsoft.Boogie {
Contract.Requires(message != null);
- if (category != null)
- {
+ if (category != null) {
message = string.Format("{0}: {1}", category, message);
}
string s;
- if (tok != null)
- {
+ if (tok != null) {
s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message);
- }
- else
- {
+ } else {
s = message;
}
- if (error)
- {
+ if (error) {
ErrorWriteLine(tw, s);
- }
- else
- {
+ } else {
tw.WriteLine(s);
}
}
@@ -1114,23 +1107,23 @@ namespace Microsoft.Boogie printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
int priority = 0;
- if (0 < CommandLineOptions.Clo.VerifySnapshots)
- {
- verificationResult = Cache.Lookup(impl, out priority);
- }
-
var wasCached = false;
- if (verificationResult != null && priority == Priority.SKIP)
- {
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
- }
+ if (0 < CommandLineOptions.Clo.VerifySnapshots) {
+ var cachedResults = Cache.Lookup(impl, out priority);
+ if (cachedResults != null && priority == Priority.SKIP) {
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start);
+ }
- printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
- wasCached = true;
+ printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+ if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) {
+ verificationResult = cachedResults;
+ wasCached = true;
+ }
+ }
}
- else
+
+ if (!wasCached)
{
#region Verify the implementation
|