summaryrefslogtreecommitdiff
path: root/Test/floats/test7.bpl
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2016-05-31 12:59:38 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2016-05-31 12:59:38 -0600
commitc19c2495497d0dfa7aaf871cf833cd5e5f986d33 (patch)
tree86c6f9fdd2baf6d8f8b2ebacda439d1ee6853dcc /Test/floats/test7.bpl
parent6f7fc01346c0ebe9072e61ace2cfede4fcedea09 (diff)
moved all the tests to the testing folder
Diffstat (limited to 'Test/floats/test7.bpl')
-rw-r--r--Test/floats/test7.bpl38
1 files changed, 38 insertions, 0 deletions
diff --git a/Test/floats/test7.bpl b/Test/floats/test7.bpl
new file mode 100644
index 00000000..8e07878d
--- /dev/null
+++ b/Test/floats/test7.bpl
@@ -0,0 +1,38 @@
+//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