diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-05-18 18:19:13 +0200 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-05-18 18:19:13 +0200 |
| commit | 216c71366e6fff4e225b68ef6ff69035c9542b4a (patch) | |
| tree | a4d11ebeb7c99d113418cf15186ce6b67923f8e4 /Source/VCGeneration/Wlp.cs | |
| parent | b8984d6c6d7495f19c70bbc1e3a364f8b0a4e206 (diff) | |
Add some experimental support for diagnosing timeouts.
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 45e511f0..82d3b607 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -118,6 +118,17 @@ namespace VC { if (ac.VerifiedUnder != null)
{
VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
+
+ if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)
+ {
+ ctxt.Ctxt.TimeoutDiagnosticIDToAssertion[ctxt.Ctxt.TimoutDiagnosticsCount] = new Tuple<AssertCmd,TransferCmd>(ac, b.TransferCmd);
+ VU = gen.Or(VU, gen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, gen.Integer(BigNum.FromInt(ctxt.Ctxt.TimoutDiagnosticsCount++))));
+ }
+ }
+ else if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)
+ {
+ ctxt.Ctxt.TimeoutDiagnosticIDToAssertion[ctxt.Ctxt.TimoutDiagnosticsCount] = new Tuple<AssertCmd,TransferCmd>(ac, b.TransferCmd);
+ VU = gen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, gen.Integer(BigNum.FromInt(ctxt.Ctxt.TimoutDiagnosticsCount++)));
}
ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
}
|