diff options
author | 2011-02-12 11:30:12 +0000 | |
---|---|---|
committer | 2011-02-12 11:30:12 +0000 | |
commit | 8926e773af99a75fe1b061a55987fa9f42898f75 (patch) | |
tree | df78081266ce1e6b3d23f710d2e8d43ab77483d9 /Source/VCGeneration | |
parent | 440d0b46604f1f83a33e861e769e1bee16baf94d (diff) |
Better support for timeout
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 7cb4b3b4..fda8770c 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -833,6 +833,9 @@ namespace VC {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ // Record current time
+ var startTime = DateTime.Now;
+
// Get the checker
Checker checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
@@ -1001,6 +1004,9 @@ namespace VC // Get the checker
Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
+ // Record current time
+ var startTime = DateTime.Now;
+
// Run live variable analysis
if (CommandLineOptions.Clo.LiveVariableAnalysis == 2)
{
@@ -1107,6 +1113,16 @@ namespace VC // case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
while (true)
{
+ // Check timeout
+ if (CommandLineOptions.Clo.ProverKillTime != -1)
+ {
+ if ((DateTime.Now - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
+ {
+ ret = Outcome.TimedOut;
+ break;
+ }
+ }
+
// Note: in the absence of a coverage graph process, the task is always "step"
coverageManager.syncGraph();
var task = coverageManager.getNextTask();
|