Problem of Non-Terminating Function (no dependencies)

Question

Using Frama-C, I am trying to slice just one source code as follows:

#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;
     }
 }
}

The slice command is the following:

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

I found the following frama-c message:

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

When I change the local variable of "BLE_msgRxBuffer" in the PB_ble_control_task() function into a global variable, I obtained a sliced code that I wanted.

1. What does the message of "no dependencies" mean?
2. Why did I obtain the sliced code that I wanted after changing the local variable of "BLE_msgRxBuffer" in the PB_ble_control_task() function into a global variable?

Answer 1

It seems your program has undefined behavior, which prevents the slicing criterion (PB_Main_event_send) from ever being called, therefore the slice trivially becomes an empty one.

To better diagnose this, I recommend using the Frama-C GUI in this case. Simply replace frama-c with frama-c-gui in your command-line.

Depending on your Frama-C version, you will either start with the default project on the GUI, or the Slicing export one. If the latter, simply go to menu Project and click default -> Set current to return to the initial (non-sliced) project.

Then go to to function PB_PacketProcess_IDLE_STATE. You should see something similar to this:

This is the result of running Eva (value analysis) in the program, which is one of the prerequisite analyses invoked by the Slicing plug-in. The red part is unreachable code. It happens precisely when trying to access buf[0], because buf contains a scalar, non-pointer value, so it cannot be dereferenced. The alarm emitted by Eva just before (mem_access: \valid_red(buf + 0)) indicates it.

Therefore, Frama-C assumes that this branch of code is never executed (no defined behaviors allow it to do so), and there are no other calls to PB_Main_event_send in the code. The Slicing plug-in rightfully concludes, therefore, that your slicing criterion is trivial, and produces the simplest program which has the equivalent behavior of never calling PB_Main_event_send, which is a mostly empty program.

This also explains your message:

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

There are no terminating defined behaviors for this function, because execution always stops at an undefined behavior. This is a major indicator that something went wrong, and therefore you should not expect your slice to be meaningful.

Fixing the code (by adding some actual memory pointed to by buf, e.g. by changing its declaration from int* msg to int msg[10]) does produce a slice that more closely resembles what one would expect from this program.

---

For a more direct answer to your first question:

The from plugin computes dependencies between function inputs and outputs. It is implicitly used by Slicing (just like Eva). Its default message is:

These dependencies hold at termination for the executions that terminate:

And then is displays the dependencies it computed.

For non-terminating functions, however, there are no such dependencies, so it simply emits "no dependencies" by default.

---

For a more direct answer to your second question:

When BLE_msgRxBuffer is a global variable, and you enable -lib-entry, its value contains not only the NULL pointer (as the default initialization of C), but also a "representative location" (see section 6.3. Describing the analysis context of the Eva plugin user manual) which can be pointed to, despite generating an alarm. Therefore, when you reach the program point mentioned above, Eva will still generate an alarm (due to NULL), but at least one execution is able to proceed without undefined behavior. Therefore the call to PB_Main_event_send is preserved, and the slicing resembles what you expected.