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/test15.bpl | |
| parent | 6f7fc01346c0ebe9072e61ace2cfede4fcedea09 (diff) | |
moved all the tests to the testing folder
Diffstat (limited to 'Test/floats/test15.bpl')
| -rw-r--r-- | Test/floats/test15.bpl | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/Test/floats/test15.bpl b/Test/floats/test15.bpl new file mode 100644 index 00000000..1dc549ac --- /dev/null +++ b/Test/floats/test15.bpl @@ -0,0 +1,24 @@ +//Translation from Muller_Kahan.c
+//Should Verify
+//NOTE: (fp(....)) causes a compiler error!
+//FAILS! Heavily...
+
+procedure main() returns () {
+ var x0 : float(11 53);
+ var x1 : float(11 53);
+ var x2 : float(11 53);
+ var i : int;
+
+ x0 := fp(11 11 53) / fp(2 11 53);
+ x1 := fp(61 11 53) / fp(11 11 53);
+ i := 0;
+ while (i < 100) {
+ x2 := fp(1130 11 53) - fp(3000 11 53) / x0;
+ x2 := fp(111 11 53) - x2 / x1;
+ x0 := x1;
+ x1 := x2;
+ i := i + 1;
+ }
+
+ assert(x0 >= fp(99 11 53) && x0 <= fp(101 11 53));
+}
\ No newline at end of file |