diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-06-07 10:24:02 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-07 10:24:02 -0600 |
| commit | 49c7d1d0133a789bb8eaa4cc0ff14c5e4493545e (patch) | |
| tree | 7af1ccd694616d41406a8f0fc550da9eff338046 /Test | |
| parent | 743be23f3961e02f1d556860f9fb0e17b98ab54d (diff) | |
removed an unnecessary type checking addition
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/floats/float3.bpl | 52 | ||||
| -rw-r--r-- | Test/test1/IntReal.bpl.expect | 4 |
2 files changed, 28 insertions, 28 deletions
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 |