diff options
author | qadeer <unknown> | 2010-09-03 21:14:04 +0000 |
---|---|---|
committer | qadeer <unknown> | 2010-09-03 21:14:04 +0000 |
commit | 918ea1673b222dc251a3588de463d164dd3e4f4d (patch) | |
tree | 79a7299a6e104a65dcafc7ebc1018a75a9ede6af /Source/VCGeneration | |
parent | 2632156b2b42feeb119288afd4c462aa946b69e3 (diff) |
Henrique's addition to the the ErrorHandler API to retrieve models
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 25 | ||||
-rw-r--r-- | Source/VCGeneration/VC.cs | 4 |
2 files changed, 29 insertions, 0 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a99fb320..c7761a37 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -382,6 +382,8 @@ namespace VC { protected string/*?*/ logFilePath;
protected bool appendLogFile;
+ public static List<ErrorModel> errorModelList;
+
public ConditionGeneration(Program p) {
Contract.Requires(p != null);
program = p;
@@ -415,6 +417,29 @@ namespace VC { return outcome;
}
+ /// <summary>
+ /// Takes an implementation and constructs a verification condition and sends
+ /// it to the theorem prover.
+ /// Returns null if "impl" is correct. Otherwise, returns a list of counterexamples,
+ /// each counterexample consisting of an array of labels.
+ /// </summary>
+ /// <param name="impl"></param>
+ public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<ErrorModel> errorsModel)
+ {
+ Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ List<Counterexample> errorsOut;
+
+ Outcome outcome;
+ errorModelList = new List<ErrorModel>();
+ outcome = VerifyImplementation(impl, program, out errorsOut);
+ errors = errorsOut;
+ errorsModel = errorModelList;
+
+ return outcome;
+ }
+
+
public Outcome StratifiedVerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 68d34547..a906f137 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2909,6 +2909,10 @@ namespace VC { public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {
//Contract.Requires(cce.NonNullElements(labels));
if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
+ if (VC.ConditionGeneration.errorModelList != null)
+ {
+ VC.ConditionGeneration.errorModelList.Add(errModel);
+ }
errModel.Print(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
|