diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-05-31 12:59:38 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-05-31 12:59:38 -0600 |
commit | c19c2495497d0dfa7aaf871cf833cd5e5f986d33 (patch) | |
tree | 86c6f9fdd2baf6d8f8b2ebacda439d1ee6853dcc /Test/floats/test10.bpl | |
parent | 6f7fc01346c0ebe9072e61ace2cfede4fcedea09 (diff) |
moved all the tests to the testing folder
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 |