Bug #8290: Функция memset не попадает в результирующий файл dismember - Verification Tool Supports - Open-Source Projects

Actions

Copy link

Bug #8290

closed

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

Added by Nikita Komarov almost 7 years ago. Updated almost 7 years ago.

Status:

Closed

Priority:

Normal

Assignee:

Denis Efremov

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

Copy link

Updated by Denis Efremov almost 7 years ago

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

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

Actions

Copy link

Updated by Denis Efremov almost 7 years ago

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

/*@ axiomatic MemSet {
    logic

Actions

Copy link

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

Copy link