diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-10-29 17:40:45 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-10-29 17:40:45 -0400 |
commit | 77123528a64dd438a31a29f8f589904d71e668e9 (patch) | |
tree | c4c49a3a17e170f69f0785996987770f4cf1ad3b /Source/VCExpr/TypeErasure.cs | |
parent | 54b058e054efe8348f8fa3d99ed5992807e28d81 (diff) | |
parent | 1f2d6c15cc587e9e1b91be70186ee9a26d5e1928 (diff) |
Merge branch 'dfsg_free'
Diffstat (limited to 'Source/VCExpr/TypeErasure.cs')
-rw-r--r-- | Source/VCExpr/TypeErasure.cs | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 76340f97..c2d99d77 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -1424,6 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null); return CastArguments(node, Type.Real, bindings, 0); } + /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArguments(node, Type.Float, bindings, 0); + }*/ public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); @@ -1472,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null); return CastArgumentsToOldType(node, bindings, 0); } + public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatRemOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMinOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMaxOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); |