Project

General

Profile

Bug #8290

Функция memset не попадает в результирующий файл dismember

Added by Nikita Komarov over 1 year ago. Updated over 1 year ago.

Status:
Closed
Priority:
Normal
Assignee:
Start date:
07/11/2017
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

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)

History

#1 Updated by Denis Efremov over 1 year ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 90

Исправлено. Требует проверки. Возможно, включаются лишние зависимости. В граф добавляются явные ребра связи не только между спецификациями и функциями, но также между спецификациями и декларациями. Стоит сделать оптимизацию, чтобы axiomatic спецификации в виде отдельного от контракта комментария не привязывались к функциям/декларациям.

#2 Updated by Denis Efremov over 1 year ago

Не должна строиться связь между MemSet -> memset. Только связь MemSet->memset_contract->memset. Влияет также на функции.

/*@ axiomatic MemSet {
    logic 

#3 Updated by Nikita Komarov over 1 year ago

А теперь на 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.

и так в бесконечном цикле

#4 Updated by Denis Efremov over 1 year ago

CRED_SEC исправлен.

#5 Updated by Denis Efremov over 1 year ago

  • % Done changed from 90 to 100

Описанная оптимизация введена в патче 2bf6bb1388a971e045596d57543ca2e9039fda85. Требует проверки.

#6 Updated by Denis Efremov over 1 year ago

  • Status changed from Resolved to Closed

Все функции buildbot корректно обрабатываются.

Also available in: Atom PDF