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

Question

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

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

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

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

Answer 1

, чтобы обнаружить некоторый код шаблона, такие как удваивается, если тесты

, если вы имеете в виду рисунок, в котором состояние внутренней, если это всегда верно потому, что он является следствием внешнего 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.