Frama-C - это платформа статического анализа с открытым исходным кодом с слайсером для программ на C , основанная на вычислении графика зависимости программ.
Обратите внимание, что нарезка реальных программ, написанных на реальныхЯзык программирования, такой как C, включает в себя множество особых случаев и понятий, которые рассматриваются в научных публикациях.Тем не менее, я уверен, что вы не найдете ничего более простого, чем вычисления PDG Frama-C, во-первых, потому что это единственный доступный Open Source (который я знаю), и во-вторых, потому что любые другие вычисления PDG, которые обрабатывают программы на C, будут иметьчтобы решить те же проблемы и ввести те же понятия.
Вот один пример:
int a, b, d, *p;
int f (int x) {
return a + x;
}
int main (int c, char **v) {
p = &b;
a = 1;
*p = 2;
d = 3;
c = f(b);
}
Команда frama-c -pdg -pdg-dot graph -pdg-print t.c создает точечные файлы graph.main.dot и graph.f.dot, содержащие PDG изmain() и f() соответственно.
Вы можете использовать программу dot для красивой печати одного из них таким образом: dot -Tpdf graph.main.dot > graph.pdf
Результат ниже:
Обратите внимание на ребро от узла c = f(b); до узла *p = 2;.Вычисления PDG, утверждающие, что они полезны для программ на Си, должны обрабатывать псевдонимы.
С другой стороны, срез, использующий этот PDG для нарезки по критерию «входы оператора c = f(b);», сможет удалить d = 3;, который не может влиять на вызов функции, даже через указатель доступа *p.Срез Frama-C использует зависимости, указанные PDG, чтобы хранить только те операторы, которые полезны для заданного пользователем критерия нарезки.Например, команда frama-c -slice-wr c t.c -then-on 'Slicing export' -print создает приведенную ниже сокращенную программу, в которой было удалено присвоение d:
/* Generated by Frama-C */
int a;
int b;
int *p;
int f_slice_1(int x)
{
int __retres;
__retres = a + x;
return (__retres);
}
void main(int c)
{
p = & b;
a = 1;
*p = 2;
c = f_slice_1(b);
return;
}