diff options
Diffstat (limited to 'float_test3.bpl')
| -rw-r--r-- | float_test3.bpl | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/float_test3.bpl b/float_test3.bpl index e93e7df7..dd0c1ba4 100644 --- a/float_test3.bpl +++ b/float_test3.bpl @@ -1,3 +1,13 @@ - procedure F() returns () { - assert fp(5) == fp(5 8 23); +//Translation from addsub_float_inexact.c +//Should give an error +procedure main() returns () { + var x : float; + var y : float; + var z : float; + var r : float; + x := fp(10000000); + y := x + fp(1); + z := x - fp(1); + r := y - z; + assert r == fp(0); }
\ No newline at end of file |