summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar allydonaldson <unknown>2013-06-19 05:17:16 +0100
committerGravatar allydonaldson <unknown>2013-06-19 05:17:16 +0100
commit970ceaa799f546b1f2c6f23ae900793752f39f50 (patch)
tree5e556f116fa742f2c406d378f3a9fbe43322939a /Source
parent53ad8fce7769a94426da4f42b319cb1b1007e1f4 (diff)
parent6fcc7aaf9259e8cff46205b1d409cf09b0007464 (diff)
Merge
Diffstat (limited to 'Source')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs124
-rw-r--r--Source/Houdini/AbstractHoudini.cs8
2 files changed, 85 insertions, 47 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 2f1e4bdc..54edf796 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -21,7 +21,8 @@ namespace Microsoft.Boogie
void AdvisoryWriteLine(string format, params object[] args);
void Inform(string s);
void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories);
- void ReportBplError(IToken tok, string message, bool error, bool showBplLocation);
+ void WriteErrorInformation(ErrorInformation errorInfo, bool isError, bool showBplLocation);
+ void ReportBplError(IToken tok, string message, bool error, bool showBplLocation, string category = null);
}
@@ -121,9 +122,27 @@ namespace Microsoft.Boogie
}
- public virtual void ReportBplError(IToken tok, string message, bool error, bool showBplLocation)
+ public void WriteErrorInformation(ErrorInformation errorInfo, bool isError, bool showBplLocation)
+ {
+ Contract.Requires(errorInfo != null);
+
+ ReportBplError(errorInfo.Tok, errorInfo.FullMsg, isError, showBplLocation);
+
+ foreach (var e in errorInfo.Aux)
+ {
+ ReportBplError(e.Tok, e.FullMsg, false, showBplLocation);
+ }
+ }
+
+
+ public virtual void ReportBplError(IToken tok, string message, bool error, bool showBplLocation, string category = null)
{
Contract.Requires(message != null);
+
+ if (category != null)
+ {
+ message = string.Format("{0}: {1}", category, message);
+ }
string s;
if (tok != null && showBplLocation)
{
@@ -165,33 +184,58 @@ namespace Microsoft.Boogie
public class ErrorInformationFactory
{
- public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null)
+ public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null)
{
Contract.Requires(tok != null);
Contract.Requires(1 <= tok.line && 1 <= tok.col);
Contract.Requires(msg != null);
- return ErrorInformation.CreateErrorInformation(tok, msg, requestId);
+ return ErrorInformation.CreateErrorInformation(tok, msg, requestId, category);
}
}
public class ErrorInformation
{
- public IToken Tok;
+ public readonly IToken Tok;
public string Msg;
+ public string Category { get; set; }
+ public string BoogieErrorCode { get; set; }
public readonly List<AuxErrorInfo> Aux = new List<AuxErrorInfo>();
public string RequestId { get; set; }
+ public string FullMsg
+ {
+ get
+ {
+ var prefix = Category;
+ if (BoogieErrorCode != null)
+ {
+ prefix = prefix == null ? BoogieErrorCode : prefix + " " + BoogieErrorCode;
+ }
+ return prefix != null ? string.Format("{0}: {1}", prefix, Msg) : Msg;
+ }
+ }
+
public struct AuxErrorInfo
{
public readonly IToken Tok;
public readonly string Msg;
+ public readonly string Category;
- public AuxErrorInfo(IToken tok, string msg)
+ public string FullMsg
+ {
+ get
+ {
+ return Category != null ? string.Format("{0}: {1}", Category, Msg) : Msg;
+ }
+ }
+
+ public AuxErrorInfo(IToken tok, string msg, string category = null)
{
Tok = tok;
Msg = CleanUp(msg);
+ Category = category;
}
}
@@ -205,19 +249,20 @@ namespace Microsoft.Boogie
Msg = CleanUp(msg);
}
- internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null)
+ internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null)
{
var result = new ErrorInformation(tok, msg);
result.RequestId = requestId;
+ result.Category = category;
return result;
}
- public virtual void AddAuxInfo(IToken tok, string msg)
+ public virtual void AddAuxInfo(IToken tok, string msg, string category = null)
{
Contract.Requires(tok != null);
Contract.Requires(1 <= tok.line && 1 <= tok.col);
Contract.Requires(msg != null);
- Aux.Add(new AuxErrorInfo(tok, msg));
+ Aux.Add(new AuxErrorInfo(tok, msg, category));
}
protected static string CleanUp(string msg)
@@ -1041,7 +1086,7 @@ namespace Microsoft.Boogie
if (CommandLineOptions.Clo.ErrorTrace > 0)
{
Console.WriteLine("Execution trace:");
- error.Print(4, b => { errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label); });
+ error.Print(4, b => { errorInfo.AddAuxInfo(b.tok, b.Label, "Execution trace"); });
}
if (CommandLineOptions.Clo.ModelViewFile != null)
{
@@ -1064,25 +1109,23 @@ namespace Microsoft.Boogie
// BP5xxx: Verification errors
ErrorInformation errorInfo;
+ var showBplLocation = true;
var callError = error as CallCounterexample;
var returnError = error as ReturnCounterexample;
var assertError = error as AssertCounterexample;
if (callError != null)
{
+ errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.", callError.RequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5002";
+ errorInfo.AddAuxInfo(callError.FailingRequires.tok, callError.FailingRequires.ErrorData as string ?? "This is the precondition that might not hold.", "Related location");
+
if (!CommandLineOptions.Clo.ForceBplErrors && callError.FailingRequires.ErrorMessage != null)
{
- printer.ReportBplError(callError.FailingRequires.tok, callError.FailingRequires.ErrorMessage, true, false);
- }
- else
- {
- printer.ReportBplError(callError.FailingCall.tok, cause + " BP5002: A precondition for this call might not hold.", true, true);
- printer.ReportBplError(callError.FailingRequires.tok, "Related location: This is the precondition that might not hold.", false, true);
+ errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingRequires.tok, callError.FailingRequires.ErrorMessage, callError.RequestId, cause);
+ showBplLocation = false;
}
- errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, cause + ": " + (callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold."), callError.RequestId);
- errorInfo.AddAuxInfo(callError.FailingRequires.tok, callError.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold.");
-
if (CommandLineOptions.Clo.XmlSink != null)
{
CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", callError.FailingCall.tok, callError.FailingRequires.tok, error.Trace);
@@ -1090,19 +1133,16 @@ namespace Microsoft.Boogie
}
else if (returnError != null)
{
+ errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5003";
+ errorInfo.AddAuxInfo(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorData as string ?? "This is the postcondition that might not hold.", "Related location");
+
if (!CommandLineOptions.Clo.ForceBplErrors && returnError.FailingEnsures.ErrorMessage != null)
{
- printer.ReportBplError(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorMessage, true, false);
- }
- else
- {
- printer.ReportBplError(returnError.FailingReturn.tok, cause + " BP5003: A postcondition might not hold on this return path.", true, true);
- printer.ReportBplError(returnError.FailingEnsures.tok, "Related location: This is the postcondition that might not hold.", false, true);
+ errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, cause);
+ showBplLocation = false;
}
- errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, cause + ": " + "A postcondition might not hold on this return path.", returnError.RequestId);
- errorInfo.AddAuxInfo(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold.");
-
if (CommandLineOptions.Clo.XmlSink != null)
{
CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", returnError.FailingReturn.tok, returnError.FailingEnsures.tok, error.Trace);
@@ -1112,9 +1152,8 @@ namespace Microsoft.Boogie
{
if (assertError.FailingAssert is LoopInitAssertCmd)
{
- printer.ReportBplError(assertError.FailingAssert.tok, cause + " BP5004: This loop invariant might not hold on entry.", true, true);
-
- errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, cause + ": " + "This loop invariant might not hold on entry.", assertError.RequestId);
+ errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not hold on entry.", assertError.RequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5004";
if (CommandLineOptions.Clo.XmlSink != null)
{
@@ -1123,9 +1162,8 @@ namespace Microsoft.Boogie
}
else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
{
- printer.ReportBplError(assertError.FailingAssert.tok, cause + " BP5005: This loop invariant might not be maintained by the loop.", true, true);
-
- errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, cause + ": " + "This loop invariant might not be maintained by the loop.", assertError.RequestId);
+ errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not be maintained by the loop.", assertError.RequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5005";
if (CommandLineOptions.Clo.XmlSink != null)
{
@@ -1134,23 +1172,20 @@ namespace Microsoft.Boogie
}
else
{
-
- var msg = assertError.FailingAssert.ErrorData as string;
if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)
{
- printer.ReportBplError(assertError.FailingAssert.tok, assertError.FailingAssert.ErrorMessage, true, false);
- }
- else if (msg != null)
- {
- printer.ReportBplError(assertError.FailingAssert.tok, msg, true, true);
+ showBplLocation = false;
}
- else
+ var msg = assertError.FailingAssert.ErrorData as string;
+ string bec = null;
+ if (msg == null)
{
msg = "This assertion might not hold.";
- printer.ReportBplError(assertError.FailingAssert.tok, cause + " BP5001: " + msg, true, true);
+ bec = "BP5001";
}
- errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, cause + ": " + msg, assertError.RequestId);
+ errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, msg, assertError.RequestId, cause);
+ errorInfo.BoogieErrorCode = bec;
if (CommandLineOptions.Clo.XmlSink != null)
{
@@ -1158,6 +1193,7 @@ namespace Microsoft.Boogie
}
}
}
+ printer.WriteErrorInformation(errorInfo, true, showBplLocation);
return errorInfo;
}
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 1be24e20..c2ff238f 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -625,9 +625,11 @@ namespace Microsoft.Boogie.Houdini {
// the right thing.
foreach (var tup in fv.functionsUsed)
{
- //var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);
- //tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);
- //prover.Assert(tt, true);
+ // Ignore ones with bound varibles
+ if (tup.Item2.InParams.Count > 0) continue;
+ var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);
+ tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);
+ prover.Assert(tt, true);
}
}