From 59052004251c655e06951eb4615938259fdf4844 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 19 Jul 2016 12:33:21 -0600 Subject: Modified the float tests to match the updated syntax --- Test/floats/float2.bpl | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'Test/floats/float2.bpl') diff --git a/Test/floats/float2.bpl b/Test/floats/float2.bpl index 1a4d02cd..ed9e60f0 100644 --- a/Test/floats/float2.bpl +++ b/Test/floats/float2.bpl @@ -1,15 +1,15 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure foo(x : float16) returns(r : float32) { - var y : float64; - var z : float128; - - r := x; // Error - r := y; // Error - r := z; // Error - y := x; // Error - y := z; // Error - z := x; // Error - - return; +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float11e5) returns(r : float24e8) { + var y : float53e11; + var z : float113e15; + + r := x; // Error + r := y; // Error + r := z; // Error + y := x; // Error + y := z; // Error + z := x; // Error + + return; } \ No newline at end of file -- cgit v1.2.3