Project

General

Profile

Actions

Bug #8290

closed

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

Added by Nikita Komarov over 7 years ago. Updated over 7 years 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)

Actions #1

Updated by Denis Efremov over 7 years ago

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

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

Actions #2

Updated by Denis Efremov over 7 years ago

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

/*@ axiomatic MemSet {
    logic 

Actions #3

Updated by Nikita Komarov over 7 years 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.

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

Actions #4

Updated by Denis Efremov over 7 years ago

CRED_SEC исправлен.

Actions #5

Updated by Denis Efremov over 7 years ago

  • % Done changed from 90 to 100

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

Actions #6

Updated by Denis Efremov over 7 years ago

  • Status changed from Resolved to Closed

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

Actions

Also available in: Atom PDF