diff options
Diffstat (limited to 'float_test8.bpl')
| -rw-r--r-- | float_test8.bpl | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/float_test8.bpl b/float_test8.bpl index 554dcf00..995ed4fa 100644 --- a/float_test8.bpl +++ b/float_test8.bpl @@ -1,3 +1,12 @@ -procedure F() returns () { - assert fp(-oo)==fp(-oo); +//Translation from float_double.c +//Should Verify +//FAILS: I don't have this functionality yet... + +procedure main() returns () { + var x : float(11 53); + var y : float; + + x := fp(100000000000000000001 11 53); + y := x; + assert(x != y); }
\ No newline at end of file |