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 | |
| parent | b8984d6c6d7495f19c70bbc1e3a364f8b0a4e206 (diff) | |
Add some experimental support for diagnosing timeouts.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/Context.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 10 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 11 |
5 files changed, 24 insertions, 3 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index da8624e9..7c690eff 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -461,7 +461,7 @@ namespace Microsoft.Boogie { Contract.Requires(cce.NonNullElements(labels));
}
- public virtual void OnResourceExceeded(string message) {
+ public virtual void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null) {
Contract.Requires(message != null);
}
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs index 83787dc5..ddc34976 100644 --- a/Source/VCGeneration/Context.cs +++ b/Source/VCGeneration/Context.cs @@ -22,6 +22,8 @@ namespace Microsoft.Boogie /// </summary>
[ContractClass(typeof(ProverContextContracts))]
public abstract class ProverContext : ICloneable {
+ public int TimoutDiagnosticsCount { get; set; }
+ public readonly Dictionary<int, Tuple<AssertCmd, TransferCmd>> TimeoutDiagnosticIDToAssertion = new Dictionary<int, Tuple<AssertCmd, TransferCmd>>();
protected virtual void ProcessDeclaration(Declaration decl) {Contract.Requires(decl != null);}
public virtual void DeclareType(TypeCtorDecl t, string attributes) {Contract.Requires(t != null); ProcessDeclaration(t); }
public virtual void DeclareConstant(Constant c, bool uniq, string attributes) {Contract.Requires(c != null); ProcessDeclaration(c); }
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index e88eb55e..69b7c8cc 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2273,7 +2273,7 @@ namespace VC { return;
}
- public override void OnResourceExceeded(string message)
+ public override void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null)
{
//Contract.Requires(message != null);
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 560f55b4..3a483a58 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2096,9 +2096,17 @@ namespace VC { return cce.NonNull((Absy)label2absy[id]);
}
- public override void OnResourceExceeded(string msg) {
+ public override void OnResourceExceeded(string msg, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null) {
//Contract.Requires(msg != null);
resourceExceededMessage = msg;
+ if (assertCmds != null)
+ {
+ foreach (var cmd in assertCmds)
+ {
+ Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);
+ callback.OnCounterexample(cex, msg);
+ }
+ }
}
public override void OnProverWarning(string msg) {
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;
}
|