diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 21:11:23 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 21:11:23 -0600 |
commit | 754f7d3ef36e11740a40a2d687f3b15195f63d9a (patch) | |
tree | 25b2ca0d03416aa6873680424fc481aeed004d67 /Test/floats/float21.bpl | |
parent | 5cff8cd77c629ec8e48a2498b1e704173306586a (diff) |
Polished up the floats test folder. Preparing to rebase
Diffstat (limited to 'Test/floats/float21.bpl')
-rw-r--r-- | Test/floats/float21.bpl | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/Test/floats/float21.bpl b/Test/floats/float21.bpl deleted file mode 100644 index 5fad5859..00000000 --- a/Test/floats/float21.bpl +++ /dev/null @@ -1,35 +0,0 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
-
-procedure main() returns () {
- var x : float32;
- var y : float32;
- var z : float32;
-
- havoc x;
- assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));
-
- if (x != TO_FLOAT32_INT(0)) {
- y := x * x;
- assert(y != TO_FLOAT32_INT(0));
- z := TO_FLOAT32_INT(1) / y;
- }
-}
-
-procedure main() returns () {
- var x : float32;
- var y : float32;
- var z : float32;
-
- havoc x;
- assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));
-
- if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) {
- y := x * x;
- assert(y != TO_FLOAT32_INT(0));
- z := TO_FLOAT32_INT(1) / y;
- }
-}
\ No newline at end of file |