Проблема нетерминирующей функции (без зависимостей)

Используя Frama-C, я пытаюсь нарезать только один исходный код следующим образом:

#include <stdio.h>
#include <stdlib.h>
#include <time.h>

typedef struct
{
 int event;
 int status;
 int* msg;
}pbBLEEvt_t;

int msgq_receive(pbBLEEvt_t *buff);

void PB_Main_event_send(int, int, void*);

static int PB_ble_ps_state = 0;

static void PB_PacketProcess_IDLE_STATE(int *buf) {
    int service_id = buf[0];
    switch (service_id) {
         case 5:
            PB_Main_event_send(0, 0, ((void *)0));
            break;
        default:
            break;
    }
}

static void PB_IncomingPacketHandler(int *buf) {
    switch (PB_ble_ps_state) {
        case 3:
            task_sleep(100);
            break;
        case 4:
            PB_PacketProcess_IDLE_STATE(buf);
            break;
        default:
            break;
    }
}

void PB_ble_control_task(void * arg) {
 int r;
 pbBLEEvt_t BLE_msgRxBuffer;

 for(;;) {
     r = msgq_receive(&BLE_msgRxBuffer);

     switch(BLE_msgRxBuffer.event) {
         case 1 :
             switch(BLE_msgRxBuffer.status) {
                 case 2 :
                     PB_IncomingPacketHandler(BLE_msgRxBuffer.msg);
                     break;
                 default:
                    break;
             }
         default:
            break;
     }
 }
}

Команда среза следующая:

SOURCE="test.c"
MAIN="PB_ble_control_task"
CALLS="PB_Main_event_send"
OUTPUT="framac_output.c"

frama-c -c11 $SOURCE -lib-entry -main $MAIN -slice-calls $CALLS -slicing-level 2 \
-then-on 'Slicing export' -print -ocode $OUTPUT \
2>&1 | tee framac_msg

Я нашел следующее сообщение frama-c:

[from] Non-terminating function PB_PacketProcess_IDLE_STATE (no dependencies)

Когда я изменяю локальную переменную «BLE_msgRxBuffer» в функции PB_ble_control_task() на глобальную переменную, я получаю нарезанный код, который мне нужен.

  1. Что означает сообщение «нет зависимостей»?
  2. Почему я получил нужный мне нарезанный код после изменения локальной переменной «BLE_msgRxBuffer» в функции PB_ble_control_task() на глобальную переменную?

c frama-c
person backpacker    schedule 24.10.2019    source источник
comment
Несколько замечаний: в показанном коде PB_ble_ps_state всегда равно нулю, поэтому PB_PacketProcess_IDLE_STATE никогда не будет вызываться, а член пакета *msg никогда не будет освобожден.   -  person Paul Ogilvie    schedule 24.10.2019
comment
Ваш пример хорош, но не идеален: требуется несколько изменений, чтобы убедиться, что он является синтаксически допустимым кодом C. Предоставление MWE увеличивает шансы на получение ответа. Это может быть полезно для будущих вопросов. В любом случае, я внес несколько изменений в код, чтобы обеспечить его компиляцию, хотя это может быть точно не тем, что вы имели в виду.   -  person anol    schedule 24.10.2019

Ответы (1)


arrow_upward
3
arrow_downward

Кажется, ваша программа имеет неопределенное поведение, которое предотвращает вызов критерия среза (PB_Main_event_send), поэтому срез тривиально становится пустым.

Чтобы лучше диагностировать это, я рекомендую использовать в этом случае графический интерфейс Frama-C. Просто замените frama-c на frama-c-gui в командной строке.

В зависимости от вашей версии Frama-C вы либо начнете с проекта default в графическом интерфейсе, либо с проекта Slicing export. Если второе, просто перейдите в меню «Проект» и нажмите default -> Set current, чтобы вернуться к исходному (не нарезанному) проекту.

Затем перейдите к функции PB_PacketProcess_IDLE_STATE. Вы должны увидеть что-то похожее на это:

Снимок экрана графического интерфейса Frama-C, показывающий, что функция критерия нарезки никогда не вызывается

Это результат выполнения Eva (анализа значений) в программе, который является одним из предварительных анализов, вызываемых подключаемым модулем Slicing. Красная часть — недостижимый код. Это происходит именно при попытке доступа к buf[0], потому что buf содержит скалярное значение, не являющееся указателем, поэтому его нельзя разыменовать. Тревога, издаваемая Евой непосредственно перед (mem_access: \valid_red(buf + 0)), указывает на это.

Следовательно, Frama-C предполагает, что эта ветвь кода никогда не выполняется (никакое определенное поведение не позволяет ей это сделать), и в коде нет других вызовов PB_Main_event_send. Таким образом, подключаемый модуль Slicing справедливо заключает, что ваш критерий нарезки тривиален, и создает простейшую программу, поведение которой эквивалентно тому, что никогда не вызывается PB_Main_event_send, что в основном является пустой программой.

Это также объясняет ваше сообщение:

[from] Non-terminating function PB_PacketProcess_IDLE_STATE (no dependencies)

Для этой функции не существует определенного поведения завершения, поскольку выполнение всегда останавливается на неопределенном поведении. Это главный показатель того, что что-то пошло не так, и поэтому не стоит ожидать, что ваш срез будет осмысленным.

Исправление кода (путем добавления некоторой фактической памяти, на которую указывает buf, например, путем изменения его объявления с int* msg на int msg[10]) действительно создает срез, который больше похож на то, что можно было бы ожидать от этой программы.

Для более прямого ответа на ваш первый вопрос:

Плагин from вычисляет зависимости между входными и выходными данными функции. Он неявно используется Slicing (как и Ева). Его сообщение по умолчанию:

These dependencies hold at termination for the executions that terminate:

А затем отображает вычисленные зависимости.

Однако для незавершающих функций таких зависимостей нет, поэтому по умолчанию он просто выдает «нет зависимостей».

Для более прямого ответа на ваш второй вопрос:

Когда BLE_msgRxBuffer является глобальной переменной, и вы включаете -lib-entry, ее значение содержит не только указатель NULL (как инициализация C по умолчанию), но и "репрезентативное местоположение" (см. раздел 6.3). . Описание контекста анализа в руководстве пользователя подключаемого модуля Eva), на который можно указать, несмотря на генерацию тревоги. Поэтому, когда вы достигнете точки программы, упомянутой выше, Ева все равно будет генерировать сигнал тревоги (из-за NULL), но по крайней мере одно выполнение сможет продолжаться без неопределенного поведения. Поэтому вызов PB_Main_event_send сохраняется, а нарезка выглядит так, как вы ожидали.

person anol    schedule 24.10.2019
comment
Часть проблемы может заключаться в том, что для функции msgq_receive не предоставлен код, который предположительно отвечает за заполнение структуры pbBLEEvt_t в соответствии с текущим обрабатываемым событием. - person Virgile; 25.10.2019