diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-07-19 12:33:21 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-07-19 12:33:21 -0600 |
| commit | 59052004251c655e06951eb4615938259fdf4844 (patch) | |
| tree | 2b11adf8766c1dc4e51a581c4ace79c84b9b4c0c /Test/floats/float8.bpl | |
| parent | 6bf5043aeab0430325c4ccde3e6ca3bd82d96704 (diff) | |
Modified the float tests to match the updated syntax
Diffstat (limited to 'Test/floats/float8.bpl')
| -rw-r--r-- | Test/floats/float8.bpl | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl index 78c11a2b..25c08e4d 100644 --- a/Test/floats/float8.bpl +++ b/Test/floats/float8.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure main() returns () {
- var x : float32;
- var y : float32;
- var z : float32;
- var r : float32;
- x := fp<8, 24>(3221225472bv32);
- y := x + fp<8, 24>(1bv32);
- z := x - fp<8, 24>(1bv32);
- r := y - z;
- assert r == fp<8, 24>(2bv32);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + var r : float24e8; + x := 0e40f24e8; + y := x + 0e0f24e8; + z := x - 0e0f24e8; + r := y - z; + assert r == 0e1f24e8; }
\ No newline at end of file |