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/test11.bpl | |
parent | 6f7fc01346c0ebe9072e61ace2cfede4fcedea09 (diff) |
moved all the tests to the testing folder
Diffstat (limited to 'Test/floats/test11.bpl')
-rw-r--r-- | Test/floats/test11.bpl | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/Test/floats/test11.bpl b/Test/floats/test11.bpl new file mode 100644 index 00000000..cee3e36e --- /dev/null +++ b/Test/floats/test11.bpl @@ -0,0 +1,55 @@ +//Translation from interpolation.c
+//Should Verify
+//Returns inconclusive? What does that mean?
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
+procedure main() returns () {
+ var i : int;
+ var z : float32;
+ var t : float32;
+ var min : [int] float32;
+ var max : [int] float32;
+
+ min[0] := TO_FLOAT32_INT(5);
+ min[1] := TO_FLOAT32_INT(10);
+ min[2] := TO_FLOAT32_INT(12);
+ min[3] := TO_FLOAT32_INT(30);
+ min[4] := TO_FLOAT32_INT(150);
+
+ max[0] := TO_FLOAT32_INT(10);
+ max[1] := TO_FLOAT32_INT(12);
+ max[2] := TO_FLOAT32_INT(30);
+ max[3] := TO_FLOAT32_INT(150);
+ max[4] := TO_FLOAT32_INT(300);
+
+ havoc t;
+ assume(t >= min[0] && t <= max[4]);
+
+ i := 0;
+ //while (i < 5) {
+ //if (t <= max[i]) {
+ //break;
+ //}
+ //i := i + 1;
+ //}
+
+ if (t > max[0]) { //1
+ i := i + 1;
+ }
+ if (t > max[1]) { //2
+ i := i + 1;
+ }
+ if (t > max[2]) { //3
+ i := i + 1;
+ }
+ if (t > max[3]) { //4
+ i := i + 1;
+ }
+ if (t > max[4]) { //5
+ i := i + 1;
+ }
+
+ z := (t - min[i]) / (max[i] - min[i]);
+
+ assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1));
+}
\ No newline at end of file |