summaryrefslogtreecommitdiff
path: root/Source/Core/StandardVisitor.cs
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-29 17:35:13 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-29 17:35:13 -0400
commit1f2d6c15cc587e9e1b91be70186ee9a26d5e1928 (patch)
tree1b6cd99944efbba2c993327bb49f2d544d50b1eb /Source/Core/StandardVisitor.cs
parent41082463d783d6f8d8a5aaf69bf459b57bca6000 (diff)
parentba4f9fa1fbd923bfce1363566af08624c5c6fe38 (diff)
Merge branch 'upstream' into dfsg_freedfsg_free
Diffstat (limited to 'Source/Core/StandardVisitor.cs')
-rw-r--r--Source/Core/StandardVisitor.cs6
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index c845a589..c3d8a672 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -103,6 +103,12 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
+ public virtual Type VisitFloatType(FloatType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this.VisitType(node);
+ }
public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);