From c19c2495497d0dfa7aaf871cf833cd5e5f986d33 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 31 May 2016 12:59:38 -0600 Subject: moved all the tests to the testing folder --- Test/floats/test12.bpl | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 Test/floats/test12.bpl (limited to 'Test/floats/test12.bpl') diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl new file mode 100644 index 00000000..c733b9f4 --- /dev/null +++ b/Test/floats/test12.bpl @@ -0,0 +1,43 @@ +//Translation from inv_Newton.c +//Should Verify +//Unfinished code! + +procedure inv(float(11 53)) returns(float(11 53)) { + var z : float(11 53); + var t : float(11 53); + var t : float(11 53); + + +} + +procedure main() returns () { + var t : float(11 53); + var t : float(11 53); + + min[0] := fp(5); + min[1] := fp(10); + min[2] := fp(12); + min[3] := fp(30); + min[4] := fp(150); + + max[0] := fp(10); + max[1] := fp(12); + max[2] := fp(30); + max[3] := fp(150); + max[4] := fp(300); + + havoc t; + assume(t >= min[0] && t <= max[4]); + + i := 0; + while (i < 5) { + if (t <= max[i]) { + break; + } + i := i + 1; + } + + z := (t - min[i]) / (max[i] - min[i]); + + assert(z >= fp(0) && z <= fp(1)); +} \ No newline at end of file -- cgit v1.2.3