--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on October 2009 ---
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); }