diff options
Diffstat (limited to 'float_test11.bpl')
| -rw-r--r-- | float_test11.bpl | 57 |
1 files changed, 37 insertions, 20 deletions
diff --git a/float_test11.bpl b/float_test11.bpl index cf9fd3a2..cee3e36e 100644 --- a/float_test11.bpl +++ b/float_test11.bpl @@ -1,38 +1,55 @@ //Translation from interpolation.c
//Should Verify
-//Returns inconclusize? What does that mean?
+//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 : float;
- var t : float;
- var min : [int] float;
- var max : [int] float;
+ var z : float32;
+ var t : float32;
+ var min : [int] float32;
+ var max : [int] float32;
- min[0] := fp(5);
- min[1] := fp(10);
- min[2] := fp(12);
- min[3] := fp(30);
- min[4] := fp(150);
+ 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] := fp(10);
- max[1] := fp(12);
- max[2] := fp(30);
- max[3] := fp(150);
- max[4] := fp(300);
+ 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;
- }
+ //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 >= fp(0) && z <= fp(1));
+ assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1));
}
\ No newline at end of file |