diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-01-04 19:26:36 -0800 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-01-04 19:26:36 -0800 |
| commit | 6fad4313b1a4e7f8e6cfcd12b92126a3d9ad58d0 (patch) | |
| tree | 7404eda3568a7f271ea2827f8e1603c139c5b452 /float_test19.bpl | |
| parent | a1c9e11736bda4bf8ea4bf431523b9b975b01670 (diff) | |
Added several test cases and some basic documentation for fp usage
Diffstat (limited to 'float_test19.bpl')
| -rw-r--r-- | float_test19.bpl | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/float_test19.bpl b/float_test19.bpl new file mode 100644 index 00000000..f00d8a2b --- /dev/null +++ b/float_test19.bpl @@ -0,0 +1,36 @@ +//Translation from flim_invariant.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;
+ }
+
+ assert(Y >= fp(-129) && Y <= fp(129));
+
+ i := i + 1;
+ }
+}
\ No newline at end of file |