Добавление кода отсутствующих функций в frama-c

Question

Добавление кода отсутствующих функций в frama-c

Прости мое невежество. Мне нужно рассчитать обратные срезы для проекта. После некоторых поисков я наткнулся на frama-c. Я скачал пакет в своей системе Ubuntu, и я получил версию Frama-c: Fluorine-20130601. Я пытаюсь использовать это впервые. При обнаружении неопределенных функций в моем проекте почти все библиотеки не определены, даже printf, scanf и т. Д. (Ни код, ни спецификация для функции printf). Согласно учебнику, я должен добавить заглушки для всех неопределенных функций. Мне действительно нужно добавлять код для каждой библиотечной функции, которую я использую, даже printf? Пожалуйста, руководство.

0

frama-c program-slicing

Источник

user6107242 02 июн '17 в 05:55

1 ответ

Решение

Другие вопросы по тегам frama-c program-slicing

user1295435 02 июн '17 в 12:55 2017-06-02 12:55 · Accepted Answer · 2017-06-02 12:55

Вам следует обновить Frama-C Phosphorus, который приносит массу улучшений в отношении функций Variadic. В частности, спецификации генерируются для функций, подобных printf / scanf, когда они вызываются в строке постоянного формата. Для невариантных функций в каталоге доступны некоторые базовые реализации $FRAMA_C_INSTALL/share/libc/*.c (в последних выпусках Frama-C).