--- layout: fc_discuss_archives title: Message 3 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,

hopefully this is not too much of a FAQ.
I first thought it would be, but I found surprisingly few sample code using
malloc (that I was able to get to run).

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;
}

When I run the yesterday released version on this code, I get

$ frama-c -val t.c
[kernel] Parsing t.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  __fc_heap_status ∈ [--..--]
  __fc_random_counter ∈ [--..--]
  __fc_rand_max ∈ {32767}
  __fc_mblen_state ∈ [--..--]
  __fc_mbtowc_state ∈ [--..--]
  __fc_wctomb_state ∈ [--..--]
[value] t.c:5: allocating variable __malloc_main_l5
[value:alarm] t.c:7: Warning: out of bounds write. assert \valid(p + 0);
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
  __fc_heap_status ∈ [--..--]
  p ∈ {‌{ &__malloc_main_l5[0] }‌}
  s[0] ∈ {0}
   [1] ∈ UNINITIALIZED
  __retres ∈ {0}
  __malloc_main_l5[0] ∈ {0}
		  [1] ∈ UNINITIALIZED

Apparently the value plugin knows about the size of the allocated chunk with
malloc. And it correctly
infers the write to s[0] as valid.
(tested by writing to s[3]! :-))

But who could I tell it to discharge the \valid(p+0) goal?

I also tried the wp plugin, but it says that allocation is not supported yet.

Thanks alot,

Holger