diff options
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
-rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 46 |
1 files changed, 38 insertions, 8 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 0c817756..1bcb6afc 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST { return Gen.Integer(node.asBigNum); } else if (node.Val is BigDec) { return Gen.Real(node.asBigDec); - } else if (node.Val is BvConst) { + } else if (node.Val is BigFloat) { + return Gen.Float(node.asBigFloat); + } + else if (node.Val is BvConst) { return Gen.Bitvector((BvConst)node.Val); } else { System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString()); @@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST { if (cce.NonNull(e.Type).IsInt) { return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e); } - else { + else {// if (cce.NonNull(e.Type).IsReal) { return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e); } + //else {//is float + //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e); + //} } else { return Gen.Not(this.args); @@ -1070,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result<VCExpr>() != null); Contract.Assert(args.Count == 2); + Type t = cce.NonNull(cce.NonNull(args[0]).Type); switch (app.Op) { case BinaryOperator.Opcode.Add: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.AddIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.AddROp, args); } + else { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "+"), args); + } case BinaryOperator.Opcode.Sub: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.SubIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.SubROp, args); } + else { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "-"), args); + } case BinaryOperator.Opcode.Mul: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.MulIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.MulROp, args); } + else + { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "*"), args); + } case BinaryOperator.Opcode.Div: return Gen.Function(VCExpressionGenerator.DivIOp, args); case BinaryOperator.Opcode.Mod: return Gen.Function(VCExpressionGenerator.ModOp, args); case BinaryOperator.Opcode.RealDiv: + if (t.IsFloat) { + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "/"), args); + } VCExpr arg0 = cce.NonNull(args[0]); VCExpr arg1 = cce.NonNull(args[1]); if (cce.NonNull(arg0.Type).IsInt) { @@ -1112,16 +1132,26 @@ namespace Microsoft.Boogie.VCExprAST { case BinaryOperator.Opcode.Eq: case BinaryOperator.Opcode.Iff: // we don't distinguish between equality and equivalence at this point + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "=="), args); return Gen.Function(VCExpressionGenerator.EqOp, args); case BinaryOperator.Opcode.Neq: return Gen.Function(VCExpressionGenerator.NeqOp, args); case BinaryOperator.Opcode.Lt: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<"), args); return Gen.Function(VCExpressionGenerator.LtOp, args); case BinaryOperator.Opcode.Le: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<="), args); return Gen.Function(VCExpressionGenerator.LeOp, args); case BinaryOperator.Opcode.Ge: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">="), args); return Gen.Function(VCExpressionGenerator.GeOp, args); case BinaryOperator.Opcode.Gt: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">"), args); return Gen.Function(VCExpressionGenerator.GtOp, args); case BinaryOperator.Opcode.Imp: return Gen.Function(VCExpressionGenerator.ImpliesOp, args); |