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/test18.bpl | 36 ------------------------------------ 1 file changed, 36 deletions(-) delete mode 100644 Test/floats/test18.bpl (limited to 'Test/floats/test18.bpl') diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl deleted file mode 100644 index 71eb5286..00000000 --- a/Test/floats/test18.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//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 -- cgit v1.2.3