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/test18.bpl | |
| parent | 6f7fc01346c0ebe9072e61ace2cfede4fcedea09 (diff) | |
moved all the tests to the testing folder
Diffstat (limited to 'Test/floats/test18.bpl')
| -rw-r--r-- | Test/floats/test18.bpl | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl new file mode 100644 index 00000000..71eb5286 --- /dev/null +++ b/Test/floats/test18.bpl @@ -0,0 +1,36 @@ +//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 |