diff options
| author |  wuestholz <unknown> | 2014-07-06 22:29:26 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-07-06 22:29:26 +0200 |
| commit | 40efa1496ae36400e0f334a215b86371a56a6b9c (patch) | |
| tree | 49a7949bff9797dbc3955af8fe9b6e744353c2ba /Source/Core | |
| parent | bb6e253feab04cc13de3132520eac3ffc8150f01 (diff) | |
Worked on adding support for "canned errors".
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 11 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 2 |
2 files changed, 12 insertions, 1 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 2f4b4e8a..e67be411 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2682,6 +2682,17 @@ namespace Microsoft.Boogie { public ISet<byte[]> AssertionChecksumsInPreviousSnapshot { get; set; }
+ public IList<AssertCmd> CannedFailingAssertions { get; protected set; }
+
+ public void AddCannedFailingAssertion(AssertCmd assertion)
+ {
+ if (CannedFailingAssertions == null)
+ {
+ CannedFailingAssertions = new List<AssertCmd>();
+ }
+ CannedFailingAssertions.Add(assertion);
+ }
+
// Strongly connected components
private StronglyConnectedComponents<Block/*!*/> scc;
[ContractInvariantMethod]
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 869c0dfa..466b2f0e 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2550,7 +2550,7 @@ namespace Microsoft.Boogie { private static Expr Conjunction(IEnumerable<Expr> conjuncts)
{
- // TODO(wuestholz): Should we use 'LiteralExpr.BinaryTreeAnd' instead?
+ // TODO(wuestholz): Maybe we should use 'LiteralExpr.BinaryTreeAnd' instead.
Expr result = null;
foreach (var c in conjuncts)
{
|