diff options
| -rw-r--r-- | Source/Doomed/DoomErrorHandler.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 30 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 4 |
6 files changed, 21 insertions, 25 deletions
diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs index a85adbe1..8d89bae3 100644 --- a/Source/Doomed/DoomErrorHandler.cs +++ b/Source/Doomed/DoomErrorHandler.cs @@ -62,7 +62,7 @@ namespace VC }
}
- public override void OnModel(IList<string>/*!>!*/ labels, Model model)
+ public override void OnModel(IList<string>/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome)
{
// TODO: it would be better to check which reachability variables are actually set to one!
List<Block> traceNodes = new List<Block>();
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 57ef660d..8b038554 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -4602,7 +4602,7 @@ namespace Microsoft.Boogie.Houdini { model = null;
}
- public override void OnModel(IList<string> labels, Model model)
+ public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)
{
Debug.Assert(model != null);
if(CommandLineOptions.Clo.PrintErrorModel >= 1) model.Write(Console.Out);
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index b5d9bc3d..fd7c1bda 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -1255,7 +1255,7 @@ namespace Microsoft.Boogie.SMTLib }
Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null :
GetErrorModel();
- handler.OnModel(xlabels, model);
+ handler.OnModel(xlabels, model, result);
}
if (labels == null || !labels.Any() || errorsLeft == 0) break;
@@ -1431,14 +1431,14 @@ namespace Microsoft.Boogie.SMTLib }
}
+
if (wasUnknown) {
SendThisVC("(get-info :reason-unknown)");
Process.Ping();
-
while (true) {
var resp = Process.GetProverResponse();
if (resp == null || Process.IsPong(resp))
- break;
+ break;
if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") {
switch (resp[0].Name) {
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index a77bfba5..9fc301da 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -461,7 +461,7 @@ namespace Microsoft.Boogie { return 0;
}
- public virtual void OnModel(IList<string> labels, Model model) {
+ public virtual void OnModel(IList<string> labels, Model model, Outcome proverOutcome) {
Contract.Requires(cce.NonNullElements(labels));
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index e37510a8..22127c5a 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1184,7 +1184,6 @@ namespace VC { if (ret == Outcome.Errors && reporter.underapproximationMode)
{
// Found a bug
- reporter.ReportErrors();
done = 2;
}
else if (ret == Outcome.Correct)
@@ -2029,9 +2028,8 @@ namespace VC { } // end FCallInliner
public class EmptyErrorHandler : ProverInterface.ErrorHandler {
- public override void OnModel(IList<string> labels, Model model) {
-
- }
+ public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)
+ { }
}
public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {
@@ -2214,12 +2212,21 @@ namespace VC { return;
}
- public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
+ public override void OnResourceExceeded(string message)
+ {
+ //Contract.Requires(message != null);
+ }
+
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {
if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
model.Write(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
+ // Timeout?
+ if (proverOutcome != ProverInterface.Outcome.Invalid)
+ return;
+
candidatesToExpand = new List<int>();
orderedStateIds = new List<Tuple<int, int>>();
var cex = GenerateTrace(labels, model, 0, mainInfo.impl, mainInfo.mvInfo);
@@ -2227,17 +2234,11 @@ namespace VC { if (underapproximationMode && cex != null) {
//Debug.Assert(candidatesToExpand.All(calls.isSkipped));
GetModelWithStates(model);
- this.CexTrace = cex;
+ callback.OnCounterexample(cex, null);
this.PrintModel(model);
}
}
- public void ReportErrors()
- {
- if(this.CexTrace != null)
- callback.OnCounterexample(this.CexTrace, null);
- }
-
private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,
int candidateId, Implementation procImpl, ModelViewInfo mvInfo) {
Contract.Requires(cce.NonNullElements(labels));
@@ -2430,11 +2431,6 @@ namespace VC { return cce.NonNull((Absy)l2a[id]);
}
- public override void OnResourceExceeded(string msg) {
- //Contract.Requires(msg != null);
- //resourceExceededMessage = msg;
- }
-
public override void OnProverWarning(string msg) {
//Contract.Requires(msg != null);
callback.OnWarning(msg);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 53868e1d..bfff8f0e 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1881,7 +1881,7 @@ namespace VC { this.program = program;
}
- public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {
//Contract.Requires(cce.NonNullElements(labels));
if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
if (VC.ConditionGeneration.errorModelList != null)
@@ -1970,7 +1970,7 @@ namespace VC { Contract.Requires(program != null);
}
- public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {
//Contract.Requires(cce.NonNullElements(labels));
// We ignore the error model here for enhanced error message purposes.
// It is only printed to the command line.
|