diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 21:09:06 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 21:09:06 -0600 |
commit | 5cff8cd77c629ec8e48a2498b1e704173306586a (patch) | |
tree | 8ab0b6fbda08b12e9b2635efdb5806371197c58c /Test/floats/test18.bpl | |
parent | c19c2495497d0dfa7aaf871cf833cd5e5f986d33 (diff) |
finished testing, fixed several minor compiler bugs
Diffstat (limited to 'Test/floats/test18.bpl')
-rw-r--r-- | Test/floats/test18.bpl | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl deleted file mode 100644 index 71eb5286..00000000 --- a/Test/floats/test18.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//Translation from rlim_exit.c
-//Should verify
-//Unary - unsupported float operations (on my end)...
-
-procedure main() returns () {
- var X : float;
- var Y : float;
- var S : float;
- var R : float;
- var D : float;
- var i : int;
-
- Y := fp(0);
-
- i := 0;
- while (i < 100000) {
- havoc X;
- havoc D;
- assume(X >= fp(-128) && X <= fp(128));
- assume(D >= fp(0) && D <= fp(16));
-
- S := Y;
- Y := X;
- R := X - S;
- if (R <= fp(0)-D) {
- Y := S - D;
- }
- else if(R >= D) {
- Y := S + D;
- }
-
- i := i + 1;
- }
-
- assert(Y >= fp(-129) && Y <= fp(129));
-}
\ No newline at end of file |