--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] beginner question about code using malloc



Dear all,

someone kindly pointed out to me, that my question got relayed to
stackoverflow.

Since the answer there was quite helpful and detailed, I thought  I
might post it here, too.

Yes, I do think mailing lists are a great medium. :-)

* Holger Kiskowski <holger.ki at freenet.de> wrote:
> How can I verify this C program using frama-c?
> 
> #include <stdlib.h>
> 
> int main(void)
> {
>   char *p = malloc(2);
>   char s[2];
>   p[0] = 0;
>   s[0] = 0;
>   return 0;
> }

--cut--
The issue is that by default, in Eva, malloc can fail. To avoid this,
choose one of the following:

1. use option -no-val-alloc-returns-null, which supposes that malloc
never fails;
2. patch the code to add a test, e.g. if (!p) exit(1);

The fact that there are 2 possible executions after the malloc is not
immediately visible in the command-line. The GUI sometimes helps when
inspecting such cases, but we can also add a call to
Frama_C_show_each(p) after the call to malloc:

char *p = malloc(2);
Frama_C_show_each_p(p);
...

Now, after running frama-c -val, we get the following line:

[value] mall.c:6: Frama_C_show_each_p: {‌{ NULL ; &__malloc_main_l5 }‌}

The two different possibilities (malloc failed and returned NULL; or malloc
succeeded and returned a new base) are considered by the analysis.

The alarm Warning: out of bounds write. assert \valid(p + 0); refers to
the first case, in which the property is invalid. The analysis stops for
this branch, which makes it harder to see what happened, since
afterwards we have a single branch, just as we had expected.
--cut--

Thanks alot for the replies (on and off-list)!

Holger