c - 非终结函数问题(无依赖性)

使用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

我发现以下frama-c消息：

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

当我将PB_ble_control_task（）函数中的“ BLE_msgRxBuffer”的局部变量更改为全局变量时，我获得了想要的分片代码。


“没有依赖项”的消息是什么意思？
将PB_ble_control_task（）函数中的“ BLE_msgRxBuffer”的局部变量更改为全局变量后，为什么获得所需的切片代码？

最佳答案

看来您的程序具有未定义的行为，这阻止了切片标准（PB_Main_event_send）的调用，因此切片变得空无一物。

为了更好地诊断此问题，我建议在这种情况下使用Frama-C GUI。只需在命令行中用frama-c替换frama-c-gui。

根据您的Frama-C版本，您可以从GUI上的default项目开始，也可以从Slicing export项目开始。如果是后者，只需转到菜单Project，然后单击default-> Set current返回到初始（未切片）项目。

然后转到功能PB_PacketProcess_IDLE_STATE。您应该看到类似以下内容：



这是在程序中运行Eva（值分析）的结果，这是Slicing插件调用的先决条件分析之一。红色部分是无法访问的代码。它恰好在尝试访问buf[0]时发生，因为buf包含标量非指针值，因此无法取消引用。 Eva在（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插件计算函数输入和输出之间的依赖关系。切片隐式使用它（就像Eva一样）。它的默认消息是：

These dependencies hold at termination for the executions that terminate:

然后显示它计算的依赖关系。

但是，对于非终止函数，不存在此类依赖关系，因此默认情况下，它仅发出“无依赖关系”。



对于第二个问题的更直接答案：

当BLE_msgRxBuffer是全局变量并且启用-lib-entry时，其值不仅包含NULL指针（作为C的默认初始化），而且还包含“代表位置”（请参见6.3节）。尽管会生成警报，但仍可以指向Eva plugin user manual的上下文。因此，当您到达上述程序点时，Eva仍会生成警报（由于NULL），但是至少可以执行一次执行而没有未定义的行为。因此，将保留对PB_Main_event_send的调用，并且切片类似于您的预期。