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

Question

Используя 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;
     }
 }
}

Команда slice выглядит следующим образом:

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

Я нашел следующую фразу-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 () на глобальную переменную?

Answer 1

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

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

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

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

Это результат запуска 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 (как Eva). Его сообщение по умолчанию:

These dependencies hold at termination for the executions that terminate:

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

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

---

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

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