diff options
author | 2015-04-27 05:37:19 -0600 | |
---|---|---|
committer | 2015-04-27 05:37:19 -0600 | |
commit | 2dae113e5996e050ca6595542de5030747245929 (patch) | |
tree | 74454d160c292949bedd02ebc1477930a763d2e1 /Source/Core | |
parent | 94a9542de594ef210d1ede1ff05e12289dfb2dc7 (diff) |
Began adding the float type to VC expression
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/AbsyExpr.cs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index a8c82f08..9297bcbc 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1706,6 +1706,10 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Real;
}
+ if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))
+ {
+ return Type.Float;
+ }
goto BAD_TYPE;
case Opcode.Div:
case Opcode.Mod:
@@ -1757,6 +1761,10 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Bool;
}
+ if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))
+ {
+ return Type.Bool;
+ }
goto BAD_TYPE;
case Opcode.And:
case Opcode.Or:
|