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