diff options
| author |  wuestholz <unknown> | 2014-06-23 23:34:23 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-06-23 23:34:23 +0200 |
| commit | 98bcde1368eb6a5df44cf252e3a2f8d8f509a0df (patch) | |
| tree | 0a6643566ab3c2e4884f1ba3f2858dd65fe8ee5a /Source/Core/Absy.cs | |
| parent | 81e96e8c695b582402a17c8957616ee72d6ebb29 (diff) | |
Worked on an extension of the existing verification result caching.
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 3b517c51..0026a3fe 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2664,6 +2664,51 @@ namespace Microsoft.Boogie { }
}
+ // TODO(wuestholz): Make this a 'List<Counterexample>'.
+ public IList<object> ErrorsInCachedSnapshot { get; set; }
+
+ public bool NoErrorsInCachedSnapshot
+ {
+ get
+ {
+ return ErrorsInCachedSnapshot != null && !ErrorsInCachedSnapshot.Any();
+ }
+ }
+
+ public bool AnyErrorsInCachedSnapshot
+ {
+ get
+ {
+ return ErrorsInCachedSnapshot != null && ErrorsInCachedSnapshot.Any();
+ }
+ }
+
+ IList<LocalVariable> injectedAssumptionVariables;
+ public IList<LocalVariable> InjectedAssumptionVariables
+ {
+ get
+ {
+ return injectedAssumptionVariables;
+ }
+ }
+
+ public Expr ConjunctionOfInjectedAssumptionVariables()
+ {
+ Contract.Requires(InjectedAssumptionVariables != null && InjectedAssumptionVariables.Any());
+
+ return LiteralExpr.BinaryTreeAnd(injectedAssumptionVariables.Select(v => (Expr)(new IdentifierExpr(Token.NoToken, v))).ToList());
+ }
+
+ public void InjectAssumptionVariable(LocalVariable variable)
+ {
+ if (injectedAssumptionVariables == null)
+ {
+ injectedAssumptionVariables = new List<LocalVariable>();
+ }
+ injectedAssumptionVariables.Add(variable);
+ LocVars.Add(variable);
+ }
+
public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)
: this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {
Contract.Requires(structuredStmts != null);
|