diff options
Diffstat (limited to 'Test/floats/test10.bpl')
-rw-r--r-- | Test/floats/test10.bpl | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/Test/floats/test10.bpl b/Test/floats/test10.bpl new file mode 100644 index 00000000..566f7a56 --- /dev/null +++ b/Test/floats/test10.bpl @@ -0,0 +1,20 @@ +//Translation from loop.c +//Should return an error? (The real case does as well...) + +procedure main() returns () { + var x : float; + var y : float; + var z : float; + + x := fp(1); + y := fp(10000000); + z := fp(42); + + while (x < y) { + x := x + fp(1); + y := y - fp(1); + z := z + fp(1); + } + + assert(z >= fp(0) && z <= fp(10000000)); +}
\ No newline at end of file |