From 5cff8cd77c629ec8e48a2498b1e704173306586a Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 21:09:06 -0600 Subject: finished testing, fixed several minor compiler bugs --- Test/floats/test12.bpl | 43 ------------------------------------------- 1 file changed, 43 deletions(-) delete mode 100644 Test/floats/test12.bpl (limited to 'Test/floats/test12.bpl') diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl deleted file mode 100644 index c733b9f4..00000000 --- a/Test/floats/test12.bpl +++ /dev/null @@ -1,43 +0,0 @@ -//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