Question

В настоящее время я открываю для себя возможности frama-c, особенно инструменты анализа WP & Value.Моя конечная цель - использовать Frama-C в больших кодах, включающих несколько слоев:

множество вызовов функций
использование сложных структур данных
статические и / или глобальные переменные

До сих пор я пытался применить восходящий метод, то есть начать указывать функции, которые не включают в себя какие-либо вызовы функций, и анализировать их поведение, изолируя их, благодаря-lib-entry и -main параметры ядра.Делая это, я проверяю, что если предварительные условия предполагаются истинными, то весь контракт функции проверяется.Как только я попытался указать верхние уровни, которые вызывают эти функции, все усложняется.Во-первых, мне часто приходится указывать поведение вызываемых функций, что не всегда легко, поскольку эти функции могут иметь дело с переменными / функциями вне области действия текущей функции.

Позвольте мне привести простой пример:Допустим, в file1.h мы определяем структуру данных «my_struct», которая содержит номер поля и четность поля.

В file1.c У меня есть две функции:

Первая функция "check_parity", которая просто проверяет, является ли поле четности статической переменной _sVar правильным.
Вторая функция "correct_parity", которая вызывает первую функцию и корректирует четность, если поле было неправильным.

В file2.c ,У меня есть функция "outside_caller", которая просто вызывает correct_parity ().Моя цель состоит в том, чтобы иметь возможность указывать outside_caller так же, как я указываю correct_parity.Ниже приведен соответствующий исходный код:

file1.h

/* parity = 0 => even ; 1 => odd */

typedef unsigned char TYP_U08;
typedef unsigned short TYP_U16;
typedef unsigned int TYP_U32;
typedef unsigned long TYP_U64;

typedef struct {
    unsigned char parity;
    unsigned int number;
} my_stuct;

typedef enum
{
    S_ERROR        =  -1
    ,S_OK          =  0
    ,S_WARNING     =  1
} TYPE_STATUS;

/*@ ghost my_stuct* g_sVar; */

/*@ predicate fc_pre_is_parity_ok{Labl}(my_stuct* i_sVar) =
        (
      \at(i_sVar->parity, Labl) == ((TYP_U08) (\at(i_sVar->number,Labl) % 2u))
    );

  @ predicate fc_pre_valid_parity{Labl}(my_stuct* i_sVar) = 
    (
        (\at(i_sVar->parity,Labl) == 0) ||
        (\at(i_sVar->parity, Labl) == 1)
    );

  @ predicate fc_pre_is_parity_readable(my_stuct* i_sVar) =
    (
        \valid_read(&i_sVar->parity)
    );

  @ predicate fc_pre_is_parity_writeable(my_stuct* i_sVar) =
    (
        \valid(&i_sVar->parity)
    );

  @ predicate fc_pre_is_number_readable(my_stuct* i_sVar) =
    (
        \valid_read(&i_sVar->number)
    );

  @ predicate fc_pre_is_number_writeable(my_stuct* i_sVar) =
    (
        \valid(&i_sVar->number)
    );
*/

TYPE_STATUS check_parity(void);
TYPE_STATUS correct_parity(void);

file1.c

static my_stuct* _sVar;

  /*@ requires check_req_parity_readable:
    fc_pre_is_parity_readable(_sVar);

    @ requires check_req_number_readable:
      fc_pre_is_number_readable(_sVar);

    @ assigns check_assigns:
      g_sVar;

    @ ensures check_ensures_error:
      !fc_pre_valid_parity{Post}(g_sVar) ==> \result == S_ERROR;

    @ ensures check_ensures_ok:
      (
        fc_pre_valid_parity{Post}(g_sVar) &&
        fc_pre_is_parity_ok{Post}(g_sVar) 
      ) ==> \result == S_OK;

    @ ensures check_ensures_warning:
      (
        fc_pre_valid_parity{Post}(g_sVar) &&
        !fc_pre_is_parity_ok{Post}(g_sVar)
      ) ==> \result == S_WARNING;

    @ ensures check_ensures_ghost_consistency:
      \at(g_sVar, Post) == _sVar;
  */
TYPE_STATUS check_parity(void)
{
    //@ ghost g_sVar = _sVar;
    TYPE_STATUS status = S_OK;
    if(!(_sVar->parity == 0 || _sVar->parity == 1)) {
        status = S_ERROR;
    } else if ( _sVar->parity == (TYP_U08)(_sVar->number % 2u) ){
        status = S_OK;
    } else {
        status = S_WARNING;
    }
  return status;
}


  /*@ requires correct_req_is_parity_writeable:
    fc_pre_is_parity_writeable(_sVar);

    @ requires correct_req_is_number_readable:
    fc_pre_is_number_readable(_sVar);

    @ assigns correct_assigns:
    _sVar->parity,
    g_sVar,
    g_sVar->parity;

    @ ensures correct_ensures_error :
    !fc_pre_valid_parity{Pre}(g_sVar) ==> \result == S_ERROR;

    @ ensures correct_ensures_ok :
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_OK;

    @ ensures correct_ensures_warning :
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      !fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_WARNING;

    @ ensures correct_ensures_consistency :
      fc_pre_is_parity_ok{Post}(g_sVar);

    @ ensures correct_ensures_validity :
      fc_pre_valid_parity{Post}(g_sVar);

    @ ensures correct_ensures_ghost_consistency :
      \at(g_sVar, Post) == _sVar;
  */
TYPE_STATUS correct_parity(void)
{
    //@ ghost g_sVar = _sVar;
    TYPE_STATUS parity_status = check_parity();

    if(parity_status == S_ERROR || parity_status == S_WARNING) {
        _sVar->parity = (TYP_U08)(_sVar->number % 2u);
        /*@ assert (\at(g_sVar->parity,Here) == 0) ||
               (\at(g_sVar->parity, Here) == 1);
     */
        //@ assert \at(g_sVar->parity, Here) == (TYP_U08)(\at(g_sVar->number,Here) % 2u);
    }
    return parity_status;
}

file2.c

/*@ requires out_req_parity_writable:
    fc_pre_is_parity_writeable(g_sVar);

  @ requires out_req_number_writeable:
    fc_pre_is_number_readable(g_sVar);

  @ assigns out_assigns:
    g_sVar,
    g_sVar->parity;

  @ ensures out_ensures_error:
    !fc_pre_valid_parity{Pre}(g_sVar) ==> \result == S_ERROR;

  @ ensures out_ensures_ok :
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_OK;

  @ ensures out_ensures_warning :
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      !fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_WARNING;

  @ ensures out_ensures_consistency:
    fc_pre_is_parity_ok{Post}(g_sVar);

  @ ensures out_ensures_validity:
    fc_pre_valid_parity{Post}(g_sVar);
*/

TYPE_STATUS outside_caller(void)
{
    TYPE_STATUS status = correct_parity();
    //@ assert fc_pre_is_parity_ok{Here}(g_sVar) ==> status == S_OK;
    /*@ assert !fc_pre_is_parity_ok{Here}(g_sVar) && 
               fc_pre_valid_parity{Here}(g_sVar) ==> status == S_WARNING; */
    //@ assert !fc_pre_valid_parity{Here}(g_sVar) ==> status == S_ERROR;
    return status;
}

Здесь основная проблема заключается в том, что для определения outside_caller () мне нужно получить доступ к _sVar, который находится вне области действия в file2.c.Это подразумевает работу с фиктивной переменной (g_sVar), которая объявлена в file1.h и обновлена в функции correct_parity.Для того, чтобы вызывающая сторона (correct_parity) могла использовать контракты вызываемых абонентов, переменная-призрак g_sVar должна использоваться внутри контрактов вызываемых абонентов .

Вот результаты анализа WP:

(1) check_parity ()

frama-c -wp src / main.c src / test.c -cpp-command 'gcc -C -E -Isrc /' -main 'check_parity' -lib-entry -wp-timeout 1 -wp-fct check_parity -wp-rte -wp-fct check_parity -then-report[rte] аннотирующая функция check_parity[wp] 14 голов запланировано[wp] Доказанные цели: 14/14Qed: 9 (4 мс)Alt-Ergo: 5 (8мс-12мс-20мс) (30)

(2) correct_parity ()

frama-c -wp src / main.c src / test.c -cpp-command 'gcc -C -E -Isrc / '-main' correct_parity '-lib-entry -wp-timeout 1 -wp-fct correct_parity -wp-rte -wp-fct correct_parity -then -report[rte] аннотирующая функция correct_parity [wp] 18 запланированных целей[wp] Доказанные цели: 18/18Qed: 12 (4 мс)Alt-Ergo: 6 (4 мс-37 мс-120 мс) (108)

(3) outside_caller ()

frama-c -wp src / main.c src / test.c -cpp-command 'gcc -C -E -Isrc / '-main' outside_caller '-lib-entry -wp-timeout 1 -wp-fct outside_caller -wp-rte -wp-fct outside_caller -then -report[rte] аннотирующая функция outside_caller[wp] 14 голов запланировано[wp] [Alt-Ergo] Цель typed_outside_caller_assign_exit: неизвестно (Qed: 4 мс) (515 мс)[wp] [Alt-Ergo] Цель typed_outside_caller_call_correct_parity_pre_correct_req_is_par___: неизвестно (636 мс)[wp] [Alt-Ergo] Цель typed_outside_caller_assert: Тайм-аут[wp] [Alt-Ergo] Цель typed_outside_caller_assign_normal_part1: время ожидания[wp] [Alt-Ergo] Цель typed_outside_caller_call_correct_parity_pre_correct_req_is_num___: неизвестно (205 мс)
[wp] Доказанные цели: 9/14
Qed: 9 (4 мс)
Alt-Ergo: 0 (прервано: 2) (неизвестно: 3)

==> WP: GUI Output

В этой конфигурации вызываемые указываются с помощью призрачной переменной g_sVar, за исключением предложений require и assings по двум причинам:

Мне нужно проверить доступ к _sVar R / W с помощью \ valid & \ valid_read, так как это указатель
Когда я попытался указать предложения присваивания вызываемых с помощью g_sVar, я не смог проверить соответствующее предложение.

Но тем самым я каким-то образом сделал спецификацию вызывающего абонента недействительной, как вы можете увидеть в выводе WP.

Почему кажется, что чем больше у меня вызовов функций, тем сложнее доказать поведение функций? Есть ли правильный способ справиться с несколькими вызовами функций и статическими переменными?

Заранее большое спасибо!

PS: Я работаю с версией Magnesium-20151002, на виртуальной машине, работающей с Ubuntu 14.04, 64-битная машина. Я знаю, что начало работы с WhyML и Why3 может мне сильно помочь, но до сих пор я не смог установить Why3 ide ни в Windows, ни в Ubuntu, выполняя каждый шаг этого учебника

Virgile · Answer 1 · 17 мая 2018

Прежде всего, обратите внимание, что -main и -lib-entry не очень полезны для WP (вы упомянули, что вы также заинтересованы в EVA / Value Analysis, но ваш вопрос направлен на WP).

Ваша проблема со статическими переменными известна, и самый простой способ ее решить - объявить в заголовке переменную-призрак. Но тогда вы должны выразить свои контракты через призрачную переменную, а не static. В противном случае абоненты не смогут использовать эти контракты, поскольку они ничего не знают о _sVar. Как правило, лучше поместить контракт в заголовок: таким образом, вы обязаны использовать только те идентификаторы, которые видны за пределами единицы перевода.

Что касается вызовов функций, главное то, что любая функция, вызываемая функцией, которую вы пытаетесь доказать с помощью WP, должна иметь контракт, который по крайней мере содержит предложение assigns (и, возможно, более точные спецификации, в зависимости от насколько влияние вызываемого абонента имеет значение для свойства, которое вы хотите доказать для вызывающего абонента). Здесь важно помнить, что с точки зрения WP, после вызова верно только то, что явно указано в контракте вызываемого абонента через ensures, плюс тот факт, что любое местоположение, не указанное в предложении assigns, было оставлено без изменений.

Frama-c: вызовы функций и статические переменные

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Frama-c: вызовы функций и статические переменные

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Похожие темы