diff options
Diffstat (limited to 'Source/Houdini')
-rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 6 | ||||
-rw-r--r-- | Source/Houdini/Checker.cs | 2 | ||||
-rw-r--r-- | Source/Houdini/Houdini.cs | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 95c29157..9f73e4a1 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -463,7 +463,7 @@ namespace Microsoft.Boogie.Houdini { }
// Remove functions AbsHoudiniConstant from the expressions and substitute them with "true"
- class ExistentialExprModelMassage : StandardVisitor
+ class ExistentialExprModelMassage : ReadOnlyVisitor
{
List<Function> ahFuncs;
@@ -491,7 +491,7 @@ namespace Microsoft.Boogie.Houdini { }
}
- class FunctionCollector : StandardVisitor
+ class FunctionCollector : ReadOnlyVisitor
{
public List<Tuple<Function, ExistsExpr>> functionsUsed;
ExistsExpr existentialExpr;
@@ -3683,7 +3683,7 @@ namespace Microsoft.Boogie.Houdini { }
- class GatherLiterals : StandardVisitor
+ class GatherLiterals : ReadOnlyVisitor
{
public List<Tuple<Variable, Expr>> literals;
bool inOld;
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 252321b6..6ffaef22 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -16,7 +16,7 @@ using VC; using System.Linq;
namespace Microsoft.Boogie.Houdini {
- public class ExistentialConstantCollector : StandardVisitor {
+ public class ExistentialConstantCollector : ReadOnlyVisitor {
public static void CollectHoudiniConstants(Houdini houdini, Implementation impl, out ExistentialConstantCollector collector)
{
collector = new ExistentialConstantCollector(houdini);
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index b05a2e5f..393c71eb 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -293,7 +293,7 @@ namespace Microsoft.Boogie.Houdini { }
}
- public class InlineEnsuresVisitor : StandardVisitor {
+ public class InlineEnsuresVisitor : ReadOnlyVisitor {
public override Ensures VisitEnsures(Ensures ensures) {
ensures.Attributes = new QKeyValue(Token.NoToken, "assume", new List<object>(), ensures.Attributes);
return base.VisitEnsures(ensures);
@@ -448,7 +448,7 @@ namespace Microsoft.Boogie.Houdini { }
// Compute dependencies between candidates
- public class CrossDependencies : StandardVisitor
+ public class CrossDependencies : ReadOnlyVisitor
{
public CrossDependencies(HashSet<Variable> constants)
{
|