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/float17.bpl | |
parent | 5cff8cd77c629ec8e48a2498b1e704173306586a (diff) |
Polished up the floats test folder. Preparing to rebase
Diffstat (limited to 'Test/floats/float17.bpl')
-rw-r--r-- | Test/floats/float17.bpl | 38 |
1 files changed, 0 insertions, 38 deletions
diff --git a/Test/floats/float17.bpl b/Test/floats/float17.bpl deleted file mode 100644 index 8e07878d..00000000 --- a/Test/floats/float17.bpl +++ /dev/null @@ -1,38 +0,0 @@ -//Translation from filter2.c -//Should give an error -//Same as the previous one; it works with reals! - -procedure main() returns () { - var E : real; - var E0 : real; - var E1 : real; - var S : real; - var S0 : real; - var S1 : real; - var i: int; - - havoc E; - havoc E0; - assume(E >= 0.0 && E <= 1.0); - assume(E0 >= 0.0 && E0 <= 1.0); - - S0 := 0.0; - S := 0.0; - - i := 0; - while (i <= 1000000) - { - E1 := E0; - E0 := E; - - havoc E; - assume(E >= 0.0 && E <= 1.0); - - S1 := S0; - S0 := S; - S := E*0.7 - E0*1.3 + E1*1.1 + S0*1.4 - S1*0.7; - - assert(S >= -4.0 && S <= 4.0); - i := i + 1; - } -}
\ No newline at end of file |