--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on October 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] dead code after an assertion unknown status



Hi Stephane,

> I cannot explain why the code immediately following the assert is seen
> as dead code.

Presumably f1 is the entry point of the analysis.
This is exactly the same situation as last time:
without any information about the argument buf,
the value analysis assumes that buf points to a fresh
variable star_buf that is not in alias with any other
variable of the program. Therefore, it is impossible to
have buf==tab and the code after the assertion is
dead. If your intention with the assertion is to force
the analysis to consider the possibility that buf points
to tab, it won't work this way (first limitation
in section 6.1.2 of the manual). The simplest way
at this time is to write a context, in C, using the
non-deterministic primitives of section 7.2.1 to
create a state that encompasses all the possibilities
that you want the analysis to consider.

> Status of the assert is "unknown" for the value analysis.

This is strange, and I will look into it if you report it as
a bug. I guess that you expected "false", and this is fair.

Note that the evaluation of the truth value of the
assertion (that results in "unknown") and the reduction
of the propagated state (that results in bottom and
causes the rest of the function to be reported as dead
code) are independent processes. On this example,
both function according to spec, only
one (the reduction) is more precise than the other
(the truth value). The truth value "unknown" is a
correct, if surprising, answer by the value analysis.

Pascal
__

char tab[10];
int f1(char* buf, int v)
{
  int i;
  //@ assert buf==tab;
  i++;
  memcpy(buf, &v, sizeof(int));
  i++;
  return *((int*)buf);
}