распространение рампы-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-с с помощью следующей команды:

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 является формальным аргументом главной точки входа. По умолчанию Value Analysis будет создавать начальное состояние, в котором такой указатель либо NULL, либо указатель на блок из двух элементов (см. Value's user manual для получения дополнительной информации о начальном состоянии анализа по умолчанию и его настройке, если необходимо). Таким образом, казалось бы, утверждение просто удалит вторую возможность и сохранит NULL как единственную возможность для colors.

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

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

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

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

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