diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-04-27 05:37:19 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-04-27 05:37:19 -0600 |
| commit | 2dae113e5996e050ca6595542de5030747245929 (patch) | |
| tree | 74454d160c292949bedd02ebc1477930a763d2e1 /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | 94a9542de594ef210d1ede1ff05e12289dfb2dc7 (diff) | |
Began adding the float type to VC expression
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 8674f8c0..aa246c37 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), e);
+ }
}
else {
return Gen.Not(this.args);
|