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: at (Holger Kiskowski)
  • Date: Sun, 3 Jun 2018 12:26:28 +0200

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}
  __retres ∈ {0}
  __malloc_main_l5[0] ∈ {0}

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,