Bug #8290
closed
Функция memset не попадает в результирующий файл dismember
Added by Nikita Komarov almost 7 years ago.
Updated almost 7 years ago.
Description
При запуске таким образом:
dismember --config ../astraver-statistics/dismember/dismember.conf --cache 1 -k ../astraver-spec -m ../astraver-spec/parsec -f pdpl_get_new -o pdpl_get_new.c
Функция: pdpl_get_new
astraver-spec: 2aca650e98f904c2c43d23f1155977271b30e513 (ветка spec)
astraver-statistics: 22a99df3448be431310a9c6bf00acd8da423038d (ветка master)
- Status changed from New to Resolved
- % Done changed from 0 to 90
Исправлено. Требует проверки. Возможно, включаются лишние зависимости. В граф добавляются явные ребра связи не только между спецификациями и функциями, но также между спецификациями и декларациями. Стоит сделать оптимизацию, чтобы axiomatic спецификации в виде отдельного от контракта комментария не привязывались к функциям/декларациям.
Не должна строиться связь между MemSet > memset. Только связь MemSet>memset_contract->memset. Влияет также на функции.
/*@ axiomatic MemSet {
logic
А теперь на CRED_SEC не работает:
Function resolve_function_declaration in C::Util::Cycle package doesn't exist. Skipping the call.
Function resolve_declaration_macro in C::Util::Cycle package doesn't exist. Skipping the call.
Can't properly resolve cycle.
и так в бесконечном цикле
- % Done changed from 90 to 100
Описанная оптимизация введена в патче 2bf6bb1388a971e045596d57543ca2e9039fda85. Требует проверки.
- Status changed from Resolved to Closed
Все функции buildbot корректно обрабатываются.
Also available in: Atom
PDF