Программа с malloc: почему Ева не может доказать \ valid (p)?

Question

Как я могу проверить эту программу на C, используя Frama-C?

#include <stdlib.h>

int main(void)
{
  char *p = malloc(2);
  char s[2];
  p[0] = 0;
  s[0] = 0;
  return 0;
}

Когда я запускаю на нем Frama-C 17 (Chlorine), точнее, плагин Eva, я получаю:

$ 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

Видимо плагин Eva знает о размере выделенного чанка с помощью malloc.И он правильно выводит запись в s[0] как действительную (например, если я пытаюсь записать в s[3], он обнаруживает ошибку).

Но как я могу сказать ему выполнить цель \valid(p+0)?

Я также попробовал подключаемый модуль WP, но он говорит, что распределение еще не поддерживается.

Answer 1

Проблема в том, что по умолчанию, в Eva, malloc может дать сбой .Чтобы избежать этого, выберите один из следующих вариантов:

• использовать параметр -no-val-alloc-returns-null, который предполагает, что malloc никогда не завершится с ошибкой;
• исправит код для добавления теста, например, if (!p) exit(1);

Подробное объяснение

Тот факт, что после malloc есть два возможных выполнения, не сразу виден в командной строке.GUI иногда помогает при проверке таких случаев, но мы также можем добавить вызов к Frama_C_show_each(p) после вызова к malloc:

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

Теперь, после запуска frama-c -val, мы получаем следующую строку:

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

При анализе учитываются две различные возможности (malloc не удалось и возвращено NULL; или malloc выполнено и возвращена новая база).

Аварийный сигналWarning: out of bounds write. assert \valid(p + 0); относится к первому случаю, в котором свойство недействительно .Анализ останавливается для этой ветви, что усложняет наблюдение за тем, что произошло, поскольку после этого у нас есть одна ветвь, как мы и ожидали.