Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] dead code after an assertion unknown status
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Wed, 14 Oct 2009 00:13:37 +0200
  • References: <1255470606.6872.7.camel@valin>
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);
}