[cfe-dev] Newby SA question

[Sergei Larin via cfe-dev]

Hello,

  I have (unexpectedly) found myself developing a specific SA checker, and during the process I run across an interesting observation.

1) The checker traces zero value passed to a specific function. That is not that important, but I based my implementation on zero arguments passed to memcpy/memset checker. Simple enough.
2) I realized that the path from function arguments to the checked function matters. Here is an example:

void test (unsigned short *, unsigned, unsigned);

void foo(const float aa[], unsigned short bb[], unsigned int cc)
{
  unsigned char dd;
  float ee = 0.f;
  for (dd = 0; dd < cc; dd++)
    ee += aa[dd];

  if (ee == 0.f)
    test(bb, 99, cc);
}


void bar(const float aa[], unsigned short bb[], unsigned int cc, unsigned int xx)
{
  unsigned char dd;
  float ee = 0.f;
  for (dd = 0; dd < cc; dd++)
    ee += aa[dd];

  if (ee == 0.f)
    test(bb, 99, xx);
}

In function foo arg cc passed to test() is SVal (0 U32b) (among other values) so my checker is triggered.
In function bar arg xx is SVal (reg_$2<unsigned int xx>) which does _not_ match zero check.

The reason for that, as far as I can read from the code, is the for() loop. In foo cc is used in (dd<cc) inequality, and value for it is estimated with a range(reg_$0<unsigned int cc> : { [0, 0] }) which at the point my checker run for test() is re-interpreted as known value of zero.

3) From #2 I can make a conclusion that presence of comparison (dd<cc above) alters analysis in a substantial way.

Now the question - is this expected behavior or a bug? If this is expected behavior is there a way to affect it with any options already available? If this is a bug, is there a mechanism to "flush" state after analysis of the for loop is over, and I want to run value estimator at the point of test() evaluation from scratch? Is there a better way to achieve determinism?


...or I simply do not know what I am talking about 😊  

Any feedback is highly appreciated. Thank you.

Sergei

--
Qualcomm Innovation Center, Inc. is a member of Code Aurora Forum, a Linux Foundation Collaborative Project.