diff options
| author |  wuestholz <unknown> | 2013-07-12 11:00:21 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-12 11:00:21 -0700 |
| commit | 714a571fee581fca2c46cf7debd9743ca1095eec (patch) | |
| tree | 0b97f697a365b26e403d416c8aafacd7ad69f780 /Source/VCGeneration/Check.cs | |
| parent | a7440ccb8d964bb99fd8772550ffd57f34064b1b (diff) | |
Worked on the parallelization.
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 66 |
1 files changed, 40 insertions, 26 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index c27d0c0d..3a8a1af9 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -178,11 +178,18 @@ namespace Microsoft.Boogie { public void Retarget(Program prog, ProverContext ctx, int timeout = 0)
{
+ lock (this)
+ {
+ hasOutput = default(bool);
+ outcome = default(ProverInterface.Outcome);
+ outputExn = default(UnexpectedProverOutputException);
+ handler = default(ProverInterface.ErrorHandler);
TheoremProver.FullReset();
ctx.Reset();
Setup(prog, ctx);
this.timeout = timeout;
SetTimeout();
+ }
}
public void SetTimeout()
@@ -288,32 +295,39 @@ namespace Microsoft.Boogie { }
private void WaitForOutput(object dummy) {
- try {
- outcome = thmProver.CheckOutcome(cce.NonNull(handler));
- } catch (UnexpectedProverOutputException e) {
- outputExn = e;
- }
-
- switch (outcome) {
- case ProverInterface.Outcome.Valid:
- thmProver.LogComment("Valid");
- break;
- case ProverInterface.Outcome.Invalid:
- thmProver.LogComment("Invalid");
- break;
- case ProverInterface.Outcome.TimeOut:
- thmProver.LogComment("Timed out");
- break;
- case ProverInterface.Outcome.OutOfMemory:
- thmProver.LogComment("Out of memory");
- break;
- case ProverInterface.Outcome.Undetermined:
- thmProver.LogComment("Undetermined");
- break;
- }
-
- hasOutput = true;
- proverRunTime = DateTime.UtcNow - proverStart;
+ lock (this)
+ {
+ try
+ {
+ outcome = thmProver.CheckOutcome(cce.NonNull(handler));
+ }
+ catch (UnexpectedProverOutputException e)
+ {
+ outputExn = e;
+ }
+
+ switch (outcome)
+ {
+ case ProverInterface.Outcome.Valid:
+ thmProver.LogComment("Valid");
+ break;
+ case ProverInterface.Outcome.Invalid:
+ thmProver.LogComment("Invalid");
+ break;
+ case ProverInterface.Outcome.TimeOut:
+ thmProver.LogComment("Timed out");
+ break;
+ case ProverInterface.Outcome.OutOfMemory:
+ thmProver.LogComment("Out of memory");
+ break;
+ case ProverInterface.Outcome.Undetermined:
+ thmProver.LogComment("Undetermined");
+ break;
+ }
+
+ hasOutput = true;
+ proverRunTime = DateTime.UtcNow - proverStart;
+ }
}
public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
|