Project

General

Profile

Bug #8290

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

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

History

#1

Updated by Denis Efremov almost 2 years ago

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

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

#2

Updated by Denis Efremov almost 2 years ago

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

/*@ axiomatic MemSet {
    logic 

#3

Updated by Nikita Komarov almost 2 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.

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

#4

Updated by Denis Efremov almost 2 years ago

CRED_SEC исправлен.

#5

Updated by Denis Efremov almost 2 years ago

  • % Done changed from 90 to 100

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

#6

Updated by Denis Efremov almost 2 years ago

  • Status changed from Resolved to Closed

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

Also available in: Atom PDF