Бесшумное поведение с параметром -rte в магнии

Question

Я сталкиваюсь с некогерентным поведением с опцией -rte в версии Magnesium (устанавливается непосредственно с ubuntu). Мне интересно, знает ли кто-нибудь об этой проблеме или что я делаю что-то неправильно.

У меня есть программа с неправильным доступом вне массива. При запуске frama-c-gui без параметров и анализа значений обнаружен доступ к внешним границам, и соответствующая аннотация отображается с оранжевым кружком. При использовании опции -rte отображаются две аннотации (для нижней и верхней границ массива), а зеленый круг отображается для обоих (что неверно).

/*@ assert rte: index_bound: 0 ≤ cpt; */ 
/*@ assert rte: index_bound: cpt < 5; */ 

Консоль говорит:

tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid. 

Я подозреваю, что существует несоответствие между двумя примечаниями, потому что они оба имеют один и тот же «имя»: index_bound.

Кроме того, часть кода после того, как цикл, содержащий дефектный доступ, окрашен в красный цвет, что указывает на то, что анализ правильно определил, что он недоступен из-за ошибки раньше.

Вот моя программа:

int main(){ 
    int t[5] = {1,2,3,4,5}; 
    int cpt =0 ; 
    int tmp ; 
    while (cpt<10){ 
    tmp = getchar() ; 
    if (t[cpt] > tmp) 
     { return 1 ; } 
    cpt++ ; 
    } 
    return 10 ; 
} 

Вот захват моего экрана (с помощью frama-c-gui -rte tableau_erreur.c).

Когда я не использую -rte вариант результат является правильным (оранжевый круг):

Я посмотрел на баг трекере, но не нашли следов, что , Мне не удалось собрать последнюю версию Frama-C, чтобы проверить ее.

Answer 1

Update: это поведение было зафиксировано в выпуске кремния Фрама-C (статус ассоциированного к утверждению rte: index_bound: cpt < 5остается неизвестной).

---

Я не мог воспроизвести точно, что вы сказали, но после запуска графического интерфейса, как в вашей команде, затем нажав на кнопку «Выполнить» в панели анализа Значение, я получил зеленые пули ,

Это эквивалентно запуску frama-c-gui -rte -then -val, в котором также отображаются зеленые (неправильные) пули.

Действительно, это кажется проблемой даже в текущей версии Frama-C, поэтому отчет об ошибке в порядке. Обратите внимание, что ручная вставка эквивалентной аннотации (//@ assert cpt < 5;) приводит к желтой пуле, как и ожидалось. Кроме того, разматывание цикла (например, с -slevel 5) также приводит к желтой пуле. Проблема, похоже, связана конкретно с использованием плагина RTE, но в любом случае она будет исследована.

С другой стороны, метка index_bound рядом с объектом не является идентификатором, а не является уникальной и не имеет отношения к проблеме.

Технические детали: Frama-С имеет понятия свойств и статусов, которые суммированы от пуль следующих к исходному коду, но более подробно описаны либо через Свойства панели (вы можете необходимо изменить некоторые фильтры и нажать на кнопку Обновить, чтобы увидеть их) или плагин Report (например, frama-c -val -then -report). В вашем примере первая итерация цикла имеет значение cpt, которое равно 0, поэтому свойство приобретает статус valid (зеленая пуля), а на последней итерации (когда cpt равно 5) он получает статус unknown (желтая пуля). По какой-то причине он был (неправильно) консолидирован как valid, отсюда и зеленая пуля. Однако в журнале значений отображается file.c:8:[value] warning: assertion 'rte,index_bound' got status unknown, который отображается на панели «Сообщения» в графическом интерфейсе. Это не объясняет ошибку, но комбинация панелей сообщений и свойств является мощным инструментом для диагностики проблем со свойствами.