diff options
author | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-06 11:29:20 +0100 |
---|---|---|
committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-06 11:29:20 +0100 |
commit | 5dcb1f8e4f28db2f449cb318fc8f114e2982cc7c (patch) | |
tree | d1a47b7f223d2db43fbb589e5f6dddc2d03c3a44 /Source/Doomed | |
parent | 6e773bb7b5dff32ca7ba552b2562ccc18b02fece (diff) | |
parent | 5fe9141ded93f6eab4e213c1d082b68ac557d81a (diff) |
merge
Diffstat (limited to 'Source/Doomed')
-rw-r--r-- | Source/Doomed/DoomCheck.cs | 3 | ||||
-rw-r--r-- | Source/Doomed/VCDoomed.cs | 8 |
2 files changed, 6 insertions, 5 deletions
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 1cbbeabf..7e2ec984 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -117,10 +117,11 @@ void ObjectInvariant() outcome = ProverInterface.Outcome.Undetermined;
Contract.Assert( m_ErrorHandler !=null);
m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
- m_Checker.ProverDone.WaitOne();
+ m_Checker.ProverTask.Wait();
try {
outcome = m_Checker.ReadOutcome();
+ m_Checker.GoBackToIdle();
} catch (UnexpectedProverOutputException e)
{
if (CommandLineOptions.Clo.TraceVerify) {
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index fadb2ea7..778ae767 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -34,8 +34,8 @@ namespace VC { /// <summary>
/// Constructor. Initializes the theorem prover.
/// </summary>
- public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program) {
+ public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, checkers) {
Contract.Requires(program != null);
this.appendLogFile = appendLogFile;
@@ -115,7 +115,7 @@ namespace VC { //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
- Checker checker = FindCheckerFor(impl, 1000);
+ Checker checker = FindCheckerFor(1000);
Contract.Assert(checker != null);
int assertionCount;
DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);
@@ -173,7 +173,7 @@ namespace VC { if (restartTP)
{
checker.Close();
- checker = FindCheckerFor(impl, 1000);
+ checker = FindCheckerFor(1000);
dc.RespawnChecker(impl, checker);
dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
}
|