Автоматическое расширение в анализе значений frama-c

Question

Я ищу метод для расширения циклов без подсказок пользователя. Я объясню на примере:

int z;
void main(void) {   
    int r = Frama_C_interval(0, MAX_INT);
    z = 0;
    for (int y=0; y<r; y++)
        z++;
}

При выполнении анализа значения frama-c для этого кода глобальная переменная z получает интервал [-, -]. Поскольку z был установлен на ноль, а цикл состоит из инкрементного оператора, метод автоматического расширения должен быть в состоянии вывести, что более точный интервал равен [0, -]. Возможно ли это сделать в Frama-C?

Answer 1

При выполнении анализа значения frama-c для этого кода глобальная переменная z получает интервал [-,-].

Нет, это не так:

~ $ frama-c -version ; echo
Magnesium-20151001+dev
~ $ cat t.c
#define MAX_INT 0x7fffffff

int z;
void main(void) {   
    int r = Frama_C_interval(0, MAX_INT);
    z = 0;
    for (int y=0; y<r; y++)
        z++;
}
~ $ frama-c -val t.c
…
t.c:8:[kernel] warning: signed overflow. assert z+1 ≤ 2147483647;
…
[value] Values at end of function main:
  z ∈ [0..2147483647]
…

Это версия для разработки, но то же самое должно применяться к любой версии, так как переполнение со знаком начало рассматриваться как серьезная ошибка с сигналом ACSL. Если вы используете версию с момента, когда подписанное переполнение предполагало безвредное получение результатов дополнения 2, 1) вам следует обновить его, это было годами и 2) z тогда вряд ли можно утверждать, что она тривиально положительна (хотя она положительна из-за реляционного инварианта, связывающего значения z а также y в то время как цикл выполняется, реляционный инвариант, который анализ значения не может представить).