Ответ 1
Frama-C - это платформа статического анализа с открытым исходным кодом с слайсер для программ на C на основе вычисления графика зависимости от программы.
Обратите внимание, что нарезанные фактические программы, написанные на реальном языке программирования, такие как C, включают в себя множество особых случаев и понятий, которые просматриваются в научных публикациях. Тем не менее, я уверен, что вы не найдете ничего проще, чем вычисление PDG Frama-C, во-первых, потому что оно является единственным открытым исходным кодом, доступным (что я знаю), а во-вторых, потому что любое другое вычисление 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 -dot-pdg graph -pdg-print t.c создает точечные файлы graph.main.dot и graph.f.dot, содержащие PDG main() и f() соответственно.
Вы можете использовать программу dot для красивой печати одного из них: dot -Tpdf graph.main.dot > graph.pdf
Результат ниже:
Обратите внимание на край от node c = f(b); до node *p = 2;. Вычисление PDG, утверждающее, что оно полезно для программ на C, должно обрабатывать сглаживание.
С другой стороны, слайсер, использующий этот 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;
}