Анализ крупных проектов с Фрама-C

Я хочу, чтобы проанализировать файл из большого проекта по созданию программы граф зависимостей, используя FRAMA-C, но продолжают получать странные ошибки, такие как:Анализ крупных проектов с Фрама-C

/usr/include/bits/fcntl-linux.h:305:[kernel] user error: Length of array is zero. This extension is unsupported

Если я пытаюсь используйте реализацию libc, предоставляемую frama-c, компиляция завершилась неудачей из-за отсутствия заголовков, таких как sys/file.h.

Я пытаюсь анализировать файлы из проекта Lynx, а именно файл в ИПВ/WWW/Библиотека/Реализация/HTTP.c, используя GCC версии 4.8.1

Что мне действительно нужно, чтобы быть в состоянии генерировать PDG для этого исходного файла (который, конечно, имеет разные зависимости), но я думаю, что если бы я мог получить даже несколько неполный график, пропустив неопределенные функции, это был бы отличный первый шаг.

источник

2013-06-14 Squatch

Возможно, вам нужно указать frama-c расположение заголовков. Это делается путем установки переменной окружения следующим образом: 'export CPP = 'gcc -C -E -I/path/to/headers -I.'' –

@CristianoSousa True (кроме того, опция GCC' -nostdinc' говорит GCC, чтобы вообще не использовать заголовки системы), но, похоже, OP это уже знает. Верно, что некоторые широко используемые заголовки не представлены в Frama-C: поставляемые Frama-C заголовки являются минимальными C-мандатными (и, возможно, некоторыми POSIX -ами). –

Вам необходимо предоставить свой файл "file.h" в каталоге "sys", размещенном в любом месте пути GCC-поиска при предварительной обработке для Frama-C.

Для справки, вот реализация sys/file.h on another system. Вы также можете быть заинтересованы в this other StackOverflow question о sys/file.h.

Для анализа стоимости FRAMA-C, в назначает пункты наряду с прототипами пройти долгий путь:

/*@ assigns *f \from ui, s, *fo; */ 
void finit(struct file *f, u_int ui, short s, void *p, struct fileops *fo);

Обратите внимание, что я понятия не имею, что функция finit() делает и будет ли выше является правильным assigns положение для него. На самом деле, в этом весь смысл: и Frama-C из коробки, и поскольку этот низкоуровневый, менее переносимый системный вызов используется в коде, который вы хотите проанализировать, кому-то нужно будет знать. Боюсь, это будет вам. С положительной стороны вам нужно только предоставить типы, макросы и прототипы функций, которые использует код, который вы хотите проанализировать.

источник

2013-06-17 07:46:13

Привет, У меня есть аналогичная проблема с ошибкой OP: '/usr/include/x86_64-linux-gnu/bits/fcntl-linux.h:316:[kernel]: Длина массива равна нулю. Это расширение не поддерживается. Я загрузил копию файла «file.h» и поместил в нее каталог с именем «sys» в одном из включенных путей, обозначенных как «export CPP =« gcc -C -E -I/path/to/headers -I ». 'to Frama-C. Тем не менее, я по-прежнему получаю ту же ошибку. Не понял ли я ваш ответ? Должен ли я делать что-то еще, чтобы решить эту проблему? Благодарю. – Benny

@Benny Да, я думаю, вы говорите о другой проблеме: «Как мне заставить Frama-C учитывать мои заголовки, а не систему?». Я не могу обвинить вас в том, что вы пытаетесь прочитать, что доступно, прежде чем задавать свой собственный вопрос, но в данном случае это другой вопрос, который следовало бы задать в другом «потоке», а не как комментарий к существующему. Ответ - «использовать -nostdinc' для предварительной обработки. Пока вы получаете сообщения об ошибках в/usr/include/x86_64-linux-gnu/..., вы по-прежнему используете неправильные заголовки, поэтому продолжайте пытаться не делать этого. –

@Benny Ваш вопрос, если бы вы его попросили, это был бы дубликат http://stackoverflow.com/q/23162014/139746 –

Анализ крупных проектов с Фрама-C

ответ

Смежные вопросы