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); }
- Follow-Ups:
- [Frama-c-discuss] dead code after an assertion unknown status
- From: stephane.duprat at atosorigin.com (Stephane DUPRAT)
- [Frama-c-discuss] dead code after an assertion unknown status
- References:
- [Frama-c-discuss] dead code after an assertion unknown status
- From: stephane.duprat at atosorigin.com (Stéphane Duprat)
- [Frama-c-discuss] dead code after an assertion unknown status
- Prev by Date: [Frama-c-discuss] dead code after an assertion unknown status
- Next by Date: [Frama-c-discuss] Beryllium does not compile on FreeBSD 7.2
- Previous by thread: [Frama-c-discuss] dead code after an assertion unknown status
- Next by thread: [Frama-c-discuss] dead code after an assertion unknown status
- Index(es):