From 49c7d1d0133a789bb8eaa4cc0ff14c5e4493545e Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 7 Jun 2016 10:24:02 -0600 Subject: removed an unnecessary type checking addition --- Source/Core/AbsyExpr.cs | 5 ++--- Test/floats/float3.bpl | 52 +++++++++++++++++++++---------------------- Test/test1/IntReal.bpl.expect | 4 ++-- 3 files changed, 30 insertions(+), 31 deletions(-) diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index b980a22b..d3e63922 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2277,7 +2277,6 @@ namespace Microsoft.Boogie { private readonly string name; private readonly Type type; private readonly Type argType; - private readonly Type argType2; private readonly int hashCode; public ArithmeticCoercion(IToken tok, CoercionType coercion) { @@ -2357,9 +2356,9 @@ namespace Microsoft.Boogie { tpInstantiation = SimpleTypeParamInstantiation.EMPTY; - if (!(cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType) || cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType2))) + if (!cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType)) { - tc.Error(this.tok, "argument type {0} does not match expected type {1} or type {2}", cce.NonNull(args[0]).Type, this.argType, this.argType2); + tc.Error(this.tok, "argument type {0} does not match expected type {1}", cce.NonNull(args[0]).Type, this.argType); } return this.type; diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl index 34059f80..240c02f3 100644 --- a/Test/floats/float3.bpl +++ b/Test/floats/float3.bpl @@ -1,27 +1,27 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure main() returns () { - var x : float32; - var y : float32; - var z : float32; - - z := x + y; - z := x - y; - z := x * y; - assume(y != fp<8, 24>(0bv32)); - z := x / y; - - z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32); - assert(z == fp<8, 24>(2bv32)); - - z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32); - assert(z == fp<8, 24>(1bv32)); - - z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23); - assert(z == fp(false, 127bv8, 0bv23)); - - z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32); - assert(z == fp(false, 127bv8, 0bv23)); - - return; +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float32; + var y : float32; + var z : float32; + + z := x + y; + z := x - y; + z := x * y; + assume(y != fp<8, 24>(0bv32)); + z := x / y; + + z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32); + assert(z == fp<8, 24>(2bv32)); + + z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32); + assert(z == fp<8, 24>(1bv32)); + + z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23); + assert(z == fp(false, 127bv8, 0bv23)); + + z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32); + assert(z == fp(false, 127bv8, 0bv23)); + + return; } \ No newline at end of file diff --git a/Test/test1/IntReal.bpl.expect b/Test/test1/IntReal.bpl.expect index b532d22a..021a8389 100644 --- a/Test/test1/IntReal.bpl.expect +++ b/Test/test1/IntReal.bpl.expect @@ -12,8 +12,8 @@ IntReal.bpl(19,12): Error: invalid argument types (real and int) to binary opera IntReal.bpl(25,8): Error: invalid argument types (int and real) to binary operator ** IntReal.bpl(29,14): Error: invalid argument types (real and int) to binary operator == IntReal.bpl(31,13): Error: invalid argument types (int and real) to binary operator == -IntReal.bpl(34,6): Error: argument type int does not match expected type real or type float -IntReal.bpl(35,6): Error: argument type real does not match expected type int or type float +IntReal.bpl(34,6): Error: argument type int does not match expected type real +IntReal.bpl(35,6): Error: argument type real does not match expected type int IntReal.bpl(47,8): Error: invalid argument types (real and int) to binary operator div IntReal.bpl(48,8): Error: invalid argument types (real and int) to binary operator mod 18 type checking errors detected in IntReal.bpl -- cgit v1.2.3