Merge pull request #5509 from piotr-grabalski/pg-wip-githubissue-5507

Add additional documentation of --nan-check flag

Author: piotr-grabalski

doc/cprover-manual/properties.md

@@ -147,6 +147,21 @@ unsigned foo(unsigned x)
   x = x + 2; // unsigned overflow checks are generated here
 ```
 
+#### Flag --nan-check limitations
+
+Please note that `--nan-check` flag is adding not-a-number checks only for
+generation of NaN value. Current implementation of `--nan-check` flag is not
+providing checks for propagation of NaN values. Generating assertions on type
+casting or structure/union member access is unsupported and such operation
+will not be examined.
+
+For example:
+
+```
+float f = 0.0/0.0; // will generate NaN - CBMC will add assertion
+float g = NAN+0.0; // propagation of NaN value - no assertion generated
+```
+
 #### Generating function bodies
 
 Sometimes implementations for called functions are not available in the goto

regression/cbmc-library/float-nan-check/main.c

@@ -0,0 +1,76 @@
+#include <assert.h>
+#include <math.h>
+#include <stdint.h>
+
+// This test contains a set of operations performed on a floating point numbers
+// to verify --nan-check flag. The result of test may change when/if support
+// of NaN value propagation checking is supported. Current behaviour of
+// --nan-check flag is that it checks whether an arithmetic operation performed
+// on a floating point value(s) is generating new not-a-number value. If NaN is
+// generated because one of the values is already NaN the assertion is not
+// produced.
+
+union container {
+  uint32_t u;
+  float f;
+};
+
+int main(void)
+{
+  // set special values
+  float mynan;
+  __CPROVER_assume(isnan(mynan));
+  float myinf;
+  __CPROVER_assume(isinf(myinf) && myinf > 0.0);
+  float myzero;
+  __CPROVER_assume(myzero == 0.0f);
+
+  // variables
+  union container c = {UINT32_MAX};
+  int n;
+
+  // should generate assertion if --nan-check flag will support
+  // NaN propagation checking
+  float g = (float)(c.u);
+  float f = c.f;
+  f = c.f + myzero;
+
+  // these operations should generate assertions
+  // 0.0 / 0.0 = NaN
+  f = myzero / myzero;
+  // n / Inf = NaN
+  f = n / (myinf);
+  // Inf * 0 = NaN
+  f = (myinf)*myzero;
+  // -Inf + Inf = NaN
+  f = (-myinf) + (myinf);
+  // Inf + (-Inf) = NaN
+  f = (myinf) + (-myinf);
+  // Inf - Inf = NaN
+  f = (myinf) - (myinf);
+  // -Inf - (-Inf) = NaN
+  f = (-myinf) - (-myinf);
+
+  // NaN + NaN = NaN
+  f = c.f + c.f;
+  // NaN / 0.0 = NaN
+  f = c.f / myzero;
+  // NaN * NaN = NaN
+  f = mynan * mynan;
+  // NaN + NaN = NaN
+  f = mynan + mynan;
+  // NaN - NaN = NaN
+  f = mynan - mynan;
+  // NaN / NaN = NaN
+  f = mynan / mynan;
+  // NAN + n = NaN
+  f = mynan + n;
+  // NAN - n = NaN
+  f = mynan - n;
+  // NAN * n = NaN
+  f = mynan * n;
+  // NAN / n = NaN
+  f = mynan / n;
+
+  return 0;
+}

regression/cbmc-library/float-nan-check/test.desc

@@ -0,0 +1,25 @@
+CORE
+main.c
+--nan-check
+\[main.NaN.1\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ myzero: SUCCESS
+\[main.NaN.2\] line \d+ NaN on / in myzero / myzero: FAILURE
+\[main.NaN.3\] line \d+ NaN on / in \(float\)n / myinf: FAILURE
+\[main.NaN.4\] line \d+ NaN on \* in myinf \* myzero: FAILURE
+\[main.NaN.5\] line \d+ NaN on \+ in -myinf \+ myinf: FAILURE
+\[main.NaN.6\] line \d+ NaN on - in myinf - myinf: FAILURE
+\[main.NaN.7\] line \d+ NaN on - in -myinf - -myinf: FAILURE
+\[main.NaN.8\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ byte_extract_little_endian\(c, (0|0l|0ll), float\): SUCCESS
+\[main.NaN.9\] line \d+ NaN on / in byte_extract_little_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS
+\[main.NaN.10\] line \d+ NaN on \* in mynan \* mynan: SUCCESS
+\[main.NaN.11\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS
+\[main.NaN.12\] line \d+ NaN on - in mynan - mynan: SUCCESS
+\[main.NaN.13\] line \d+ NaN on / in mynan / mynan: SUCCESS
+\[main.NaN.14\] line \d+ NaN on \+ in mynan \+ \(float\)n: SUCCESS
+\[main.NaN.15\] line \d+ NaN on - in mynan - \(float\)n: SUCCESS
+\[main.NaN.16\] line \d+ NaN on \* in mynan \* \(float\)n: SUCCESS
+\[main.NaN.17\] line \d+ NaN on / in mynan / \(float\)n: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+\[main.NaN.18\]