frama-c останавливает распространение: "Утверждение получило статус недействительный"

Question

Я хочу нарезать файл test.c для всех утверждений.

test.c выглядит следующим образом:

#include <stdlib.h>

typedef struct {
   float r;
   float g;
   float b;
} Color;

typedef struct {
   int k;
   Color* colors;
} Colors;

void foo(int* a, int k, Colors *colors)
{
    int b=0;   
    colors->colors = (Color*) malloc(k*sizeof(Color));
    //@ assert (colors == NULL);
    if (colors==NULL)
        return;

    colors->k = k;
    int c=10;
    *a=8;
    //@ assert(*a>b);
}

Я запускаю frama-c с помощью следующей команды:

frama-c -slice-assert @all -main foo test.c -then-on 'Slicing export' -print -ocode slice.c

Результирующий slice.c выглядит следующим образом:

/* Generated by Frama-C */
typedef unsigned int size_t;
struct __anonstruct_Color_1 {
   float r ;
   float g ;
   float b ;
};
typedef struct __anonstruct_Color_1 Color;
struct __anonstruct_Colors_2 {
   int k ;
   Color *colors ;
};
typedef struct __anonstruct_Colors_2 Colors;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;

  }
 */
void foo(int *a, Colors *colors)
{
  int b;
  /*@ assert colors ≡ (Colors *)((void *)0); */ ;
  return;
}

Глядя на функцию нарезки fooкажется, что обработка была как-то неполной. Вывод frama-c говорит мне:

test.c:19:[kernel] warning: out of bounds write. assert \valid(&colors->colors);
test.c:20:[value] Assertion got status invalid (stopping propagation).

Что означает "неверный статус"? Почему это перестает распространяться здесь и почему это работает, когда я изменяю первое утверждение на //@ assert (colors != NULL);?

Answer 1

Подключаемый модуль Slicing опирается на информацию, вычисленную с помощью Value Analysis. В ходе своего запуска Value Analysis пытается оценить любую аннотацию ACSL, присутствующую в исследуемых ветвях. Это в особенности касается assert colors == NULL; в вашем примере, который действительно считается недействительным.

Это почему? Во-первых, мы можем отметить, что colors является формальным аргументом главной точки входа. По умолчанию анализ значений создает исходное состояние, в котором указатель NULL или указатель на блок из двух элементов (см . руководство пользователя Value для получения дополнительной информации о начальном состоянии анализа по умолчанию и о том, как его можно настроить при необходимости). Таким образом, казалось бы, что утверждение просто удалит вторую возможность и сохранит NULL как единственная возможность для colors,

Однако есть еще одна вещь, с которой работает функция colors до достижения assert: это назначает что-то в colors->colors, Для того, чтобы это назначение было действительным, colors необходимо указать на правильное место в памяти. Отсюда и предупреждение, которое вы видите в строке 19 (по-видимому, выдаваемое ядром по историческим причинам, но в действительности испускаемое Value), материализованное генерацией другого утверждения, \valid(&colors->colors), что вы можете увидеть, если вы запустите frama-c-gui с вашими вариантами.

После подачи тревоги Value пытается уменьшить свое внутреннее состояние в соответствии с ним, так как конкретное выполнение может идти дальше (без риска в земле неопределенного поведения), если оно проверяет данное условие. В нашем случае это означает удаление NULL для набора возможных значений для colors, Следовательно, когда мы сталкиваемся с утверждением, у нас есть только одна возможность для colorsи, поскольку он не соответствует утверждению, статус недействителен, и распространение остановлено: никакое конкретное выполнение не может достичь этой точки и проверить утверждение.

ОБНОВЛЕНИЕ Если вы измените первое утверждение на //@ assert (colors != NULL);Анализ значений покажет, что он действителен, поскольку, как сказано выше, достижение точки, в которой оценивается утверждение, может быть сделано только с действительным colors указатель из-за colors->colors в предыдущей инструкции. Таким образом, Value приступает к анализу, а нарезка выполняется по программе, которая обычно завершается, что приводит к ожидаемому результату.

Что касается вашего комментария, аннотация ACSL действительна, если во время какого-либо конкретного выполнения программы, которая проходит через аннотацию, она оценивается как истинная, а в противном случае недействительной (и выполнение должно прекратиться в случае, если аннотация оценивается как ложная). На практике часто невозможно (по крайней мере, не в разумное количество времени и / или памяти) выполнить все такие оценки, отсюда и неизвестный статус, что означает, что плагин не может принять решение. Обратите внимание, что в любом случае статус, предоставляемый данным плагином, зависит от конфигурации этого плагина. Например, для значения выбранная точка входа и начальная конфигурация влияют на состояние достоверности аннотаций, с которыми сталкивается значение во время его абстрактного выполнения. Точнее говоря, каждый раз, когда абстрактное выполнение достигает аннотации, статус вычисляется следующим образом:

• если аннотация истинна для всех конкретных состояний, представленных текущим абстрактным состоянием, то выдается действительный статус.
• если аннотация является ложной для всех таких конкретных состояний, выводится недопустимый статус, и абстрактное выполнение останавливается для этой ветви (так как никакое конкретное выполнение не будет проходить после аннотации).
• в противном случае статус неизвестен: Value не может знать, могут ли конкретные состояния, для которых аннотация оценивается как ложная, действительно иметь место на практике или являются просто артефактом приближений, сделанных до сих пор. Однако он пытается уменьшить свое абстрактное состояние, чтобы оно представляло как можно меньше недопустимых состояний (например, если у вас есть /*@ assert 0<= x <= 10;*/ а также x как известно, находится в интервале [3; 17]Значение будет использовать [3; 10] за интервал x после утверждения).