Frama-C прервана Неверный ввод пользователя

Question

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

The error shows as 
"fatal error: event.h: No such file or directory. Compilation terminated".

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)

[kernel] Parsing WorkSpace/bipbuffer.c (with preprocessing)

[kernel] user error: failed to run: gcc -E -C -I.  -dD -D__FRAMAC__  -nostdinc -D__FC_MACHDEP_X86_32 -I/usr/share/frama-c/libc -o '/tmp/bipbuffer.ce6d077.i' '/home/xxx/WorkSpace/bipbuffer.c'    you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".

[kernel] user error: stopping on file "/home/xxx/WorkSpace/bipbuffer.c" that has errors. Add'-kernel-msg-key pp' for preprocessing command.

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

Я думал, что это потому, что у меня не было зависимостей 'event.h', но он все еще возвращает эти ошибки после того, как я установил зависимости libevent. Я не уверен, нужно ли мне вручную устанавливать какой-либо путь зависимостей для frama-c

Вот часть файла C (Ссылка на источник: https://memcached.org/), который я хотел бы открыть:

#include "stdio.h"
#include <stdlib.h>

/* for memcpy */
#include <string.h>

#include "bipbuffer.h"

static size_t bipbuf_sizeof(const unsigned int size)
{
    return sizeof(bipbuf_t) + size;
}

int bipbuf_unused(const bipbuf_t* me)
{
    if (1 == me->b_inuse)
        /* distance between region B and region A */
        return me->a_start - me->b_end;
    else
        return me->size - me->a_end;
}
......

Спасибо

Answer 1

В дополнение к ответу Изабель Ньюби, я хотел бы отметить, что версия Frama-C для Chlorine, бета-версия которой была недавно анонсирована , имеет новую опцию -json-compilation-database, которая пытается прочитать аргументы для передачи препроцессору из базы данных компиляции .

Такая база данных может быть сгенерирована непосредственно с помощью cmake, но существуют решения для проекта на основе make, такого как тот, на который вы ссылаетесь, в частности bear , который перехватывает команды, запускаемые make для построения базы данных.

Answer 2

Вот подробное описание того, как вы могли бы продолжить, используя новую опцию -json-compilation-database из Frama-C 17 Chlorine, плюс дополнительный скрипт list_files.py (которого нет в бета-версии, но он будет доступен в финальной версии 17релиз и может быть загружен здесь ):

1. Получите исходные файлы, которые вы хотите проанализировать с помощью Frama-C, запустите ./configure и, если возможно, попробуйтеотключить необязательные зависимости от внешних библиотек;например, некоторые базы кода включают необязательные зависимости, основанные на доступности библиотек / системных функций, но имеют запасные варианты (прибегая к стандартной библиотеке C или функциям POSIX).Чем больше вы дадите Frama-C, тем больше шансов хорошо его проанализировать, поэтому, если такие внешние библиотеки не являются необходимыми, исключение их может помочь получить более «код POSIXy», что должно помочь.Обычно это видно в файлах config.h, в макросах, обычно называемых HAVE_*.

2. Скомпилируйте и установите Создайте EAR или другой эквивалентный инструмент для получения compile_commands.json file.

3. Запустите bear make (или cmake с флагом CMAKE_EXPORT_COMPILE_COMMANDS), чтобы получить файл compile_commands.json.

4. Запуститеlist_files.py в каталоге, содержащем compile_commands.json, для получения списка источников C, использованных во время компиляции.

5. Запустите Frama-C (17 Chlorine или новее), предоставив ему списокисточники, найденные на предыдущем шаге, плюс опция -json-compilation-database . для анализа compile_commands.json и, надеюсь, получения соответствующих флагов предварительной обработки.

В идеале этого должно быть достаточно, но на практикеэто достаточно редко.В частности, из-за наличия внешних библиотек и функций не-C99, не-POSIX, всегда необходимы следующие шаги:

6.Включение внешних библиотек

На этом этапе Frama-C будет жаловаться на отсутствие event.h.Вы должны будете включить заголовки этой библиотеки самостоятельно. Примечание: копирование заголовков непосредственно из /usr/include, скорее всего, не будет работать из-за нескольких специфических для архитектуры определений, особенно таких файлов, как bits/*.h. .

Вместо этого рассмотрите возможность загрузки внешних библиотек и их подготовки (например, запуск по крайней мере ./configure).Затем вручную добавьте дополнительный каталог включения с помощью -cpp-extra-args="-I <path/to/your/sources/for/libevent.h>/include".

7.Включение отсутствующих заголовков, отличных от POSIX

Могут отсутствовать некоторые другие заголовки, в частности источники, специфичные для GNU или BSD (например, sysexits.h).Получить эти заголовки и добавить их при необходимости.Сообщение об ошибке в этом случае исходит от препроцессора (gcc) и выглядит так:

memcached.c:51:10: fatal error: sysexits.h: No such file or directory
 #include <sysexits.h>
          ^~~~~~~~~~~~
compilation terminated.

8.Определение отсутствующих не-POSIX-типов и констант

На этом этапе все необходимые заголовки должны быть доступны, но синтаксический анализ с Frama-C все еще может завершиться неудачей.Это связано с использованием определений не-POSIX-типа (например, caddr_t, struct ling), не-POSIX-констант (например, MAXPATHLEN, SOCK_NONBLOCK, NI_MAXSERV).Сообщения об ошибках, как правило, напоминают следующее:

[kernel] memcached.c:3261: Failure: Cannot resolve variable MAXPATHLEN

Константы часто легко предоставить вручную, сгребая то, что доступно в ваших /usr/include.

Определениях типов, с другой стороны, может потребоватьсянекоторые вставки копий в нужных местах, особенно если они зависят от других типов, которые также отсутствуют.Этот шаг вряд ли можно автоматизировать, но он довольно прост, если вы привыкнете к некоторым конкретным сообщениям об ошибках.

Например, следующее сообщение об ошибке связано с отсутствующим определением типа (caddr_t):

[kernel] Parsing memcached.c (with preprocessing)
[kernel] memcached.c:1074: 
  syntax error:
  Location: line 1074, between columns 38 and 47, before or at token: c
  1072          *hdr++ = 0;
  1073          *hdr++ = 0;
  1074          assert((void *) hdr == (caddr_t)c->msglist[i].msg_iov[0].iov_base + UDP_HEADER_SIZE);
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  1075      }
  1076

Обратите внимание, что токен перед c - это (caddr_t), который никогда не определялся (его часто определяют как void * или char *).

Следующее сообщение об ошибке:относится к неполному типу, то есть struct, используемому где-то, но никогда не определенному:

[kernel] memcached.c:5811: User Error: 
  variable `ling' has initializer but incomplete type

Это означает, что тип переменной ling, который равен struct linger (не POSIX), никогда не был определен.В этом случае мы можем скопировать его с нашего /usr/include/bits/socket.h:

struct linger
  {
    int l_onoff;            /* Nonzero to linger on close.  */
    int l_linger;           /* Time to linger.  */
  };

Примечание: если в libc Frama-C отсутствуют константы / определения POSIX, рассмотрите возможность уведомления их разработчиков или предложения запросов на извлечение в Github Frama-C.

9. Исправление несовместимых и отсутствующих прототипов функций

Синтаксический анализ, вероятно, завершится успешно после предыдущего шага, но он может все же завершиться ошибкой из-за несовместимых прототипов функций. Например, вы можете получить:

[kernel] User Error: Incompatible declaration for usleep:
  different integer types int and unsigned int
  First declaration was at assoc.c:238
  Current declaration is at items.c:1573

Это следствие предупреждения, выпущенного ранее:

[kernel:typing:implicit-function-declaration] slabs.c:1150: Warning: 
  Calling undeclared function usleep. Old style K&R code?

Это означает, что вызывается функция usleep, но у нее нет прототипа, поэтому Frama-C использует соглашение о неявном int до C99: оно генерирует такой прототип, но позже в коде фактическое объявление usleep найдено, и его тип не int. Отсюда и ошибка.

Чтобы предотвратить это, вы должны убедиться, что прототип usleep правильно включен. Поскольку это , а не POSIX.1-2008, вам необходимо либо определить / отменить определение соответствующих макросов (см. unistd.h), либо добавить свой собственный прототип.

В конце это должно позволить Frama-C проанализировать файлы и создать AST.

Однако, есть еще несколько пропущенных прототипов; нам просто повезло, что ни один из них не вступал в противоречие с реальными заявлениями. В идеале вы должны считать этап синтаксического анализа выполненным, когда больше нет сообщений, таких как implicit-function-declaration и подобных предупреждений.

Некоторые из отсутствующих прототипов в memcached, такие как getsubopt, являются POSIX и должны быть интегрированы в стандартную библиотеку Frama-C. Другие могут составить часть небольшой библиотеки нестандартных заглушек, которая будет использоваться для другого программного обеспечения.

Содействие с результатами для повторного использования в будущем

Успешного завершения этапа синтаксического анализа для таких библиотек с открытым исходным кодом достаточно, чтобы рассмотреть их для интеграции в этот репозиторий примеров с открытым исходным кодом , чтобы будущие пользователи могли начать анализ без необходимости повторять все эти шаги. ( Хранилище ориентировано на Eva, но не исключительно: разбор полезен для всех плагинов Frama-C. )

Answer 3

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

Вам необходимо выяснить, где установлен event.h, а затем передать что-то вроде -cpp-extra-args "-I /path/to/directory/" Frama-C. Передайте только имя каталога, не включая имя event.h.