diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-07-13 19:40:09 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-07-13 19:40:09 -0600 |
| commit | 52aa9b8f63a3d955031e7a0dfd6e575ca7cf76b3 (patch) | |
| tree | b24be506dda4eae8b2f98486ddacd8df031dc119 /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | fe331e0a63c7921a996e007860182bad9628fb0d (diff) | |
Modified internal abstract float representation to allow user-defined mantissa and exponent
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 942116eb..f0dc505d 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1005,12 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST { if (cce.NonNull(e.Type).IsInt) {
return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);
}
- else if (cce.NonNull(e.Type).IsReal) {
+ 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 {//is float
+ //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e);
+ //}
}
else {
return Gen.Not(this.args);
|