diff options
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)); |