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] beginner question about code using malloc

  • Subject: [Frama-c-discuss] beginner question about code using malloc
  • From: holger.ki at freenet.de (Holger Kiskowski)
  • Date: Mon, 25 Jun 2018 21:03:55 +0200
  • In-reply-to: <20180603102628.GA2254@localhost>
  • References: <20180603102628.GA2254@localhost>
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