Проверка типа и обнаружение кода кода, Frama-C

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

Или, может быть, что-то, использующее имена переменных, например, проверьте, принадлежит ли переменная с заданным префиксным именем к определенному типу.

Как вы думаете, возможно ли это с помощью Frama-C (с использованием ACSL или путем разработки нового модуля)?

Спасибо большое =)

1 ответ

для обнаружения некоторого кода кода, такого как удвоение, если тесты

если вы имеете в виду шаблон, в котором условие внутреннего if всегда истинно, потому что оно является следствием внешнего if, GUI уже может показать вам, что внутренняя ветвь if else оказалась недостижимой во время анализ стоимости.

Для простого примера:

int x, y;
int main(int c){
 if (c == 2)
 {
 x = x * c;
 if (c == 2)
 {
 y = y * c;
 }
 else
 {
 y = y / c;
 }
 }
}

Командная строка:

$ frama-c-gui -val t.c

Это можно использовать только эвристически. Детектор звука для избыточных тестов, разделенных траекторией выполнения, по которой переменные, которые не были изменены, может быть реализован как плагин, используя результаты анализа значения.

что вызов данной функции всегда сопровождается другим.

Это возможно, используя Aoraï, плагин Frama-C, который (EDITED:) включен в дистрибутив Frama-C, несмотря на что утверждает его веб-страница. Aoraï генерирует доказательные обязательства, которые соответствуют выраженному временному свойству. Доказательство этих обязательств может быть более или менее трудным. В некотором смысле Aoraï только уменьшает проблему проверки временных свойств на другую проблему, для которой есть плагины в Frama-C.

проверить, принадлежит ли переменная с заданным префиксным именем к определенному типу.

Этот тип "стандарта кодирования" может быть реализован как плагин Frama-C. Atos внедрил плагин под названием Taster, чтобы проверить правила кодирования Airbus.

licensed under cc by-sa 3.0 with attribution.