Potentially unprotected variable

#include <limits.h>
int shared_var;

void inc() {
    shared_var+=2;
}

void reset() {
    shared_var = 0;
}

void task() {
    volatile int randomValue = 0;
    while(randomValue) {
        reset();
        inc();
        inc();
    }
}

void interrupt() {
    shared_var = INT_MAX;
}

void interrupt_handler() {
    volatile int randomValue = 0;
    while(randomValue) {
        interrupt();
    }
}

void main() {
}

In this example, shared_var is an unprotected shared variable if you specify the following multitasking options:

Option	Value
Configure multitasking manually
Tasks	task interrupt_handler

You do not specify protection mechanisms such as critical sections.

The operation shared_var = INT_MAX can interrupt the other operations on shared_var and cause unpredictable behavior.

If you click the (graph) icon on the Result Details pane, you see the two concurrent tasks (threads).

The first graph shows how the tasks access the variable. For instance, the task interrupt_handler calls a function interrupt that writes to the shared variable shared_var.

The second graph shows how the tasks are created. In this example, both tasks are created after main completes. In other cases, tasks might be created within functions called from main.

#include <stdio.h>
#include <stdlib.h>
#define SIZE_ARRAY 3

typedef unsigned int uint32;

// Defining three functions of which 
// only one accesses a global variable
uint32 var;

void Write_to_var(void) {
    var+=1;
}

void No_write_read_1(void) {
}

void No_write_read_2(void) {
   
}

// Defining a 3-element array of function pointers 
// that point to the three functions
typedef void (*FuncPtr)(void);
typedef struct {
    FuncPtr pFuncPtr;
}FuncPtrStruct;

const FuncPtrStruct FuncPtrArray[SIZE_ARRAY] =
{
    { &Write_to_var    },
    { &No_write_read_1 },
    { &No_write_read_2 }
};

void main() {}

// Defining a function that calls one of the three functions 
// via the function pointer
void function(int uiSignalType) {
    FuncPtrArray[uiSignalType].pFuncPtr();
}

// Entry-point functions in void(void) format for Polyspace analysis
// Analyze this example with
// -D POLYSPACE -entry-points task_10ms,task_20ms,task_50ms

#ifdef POLYSPACE
void task_10ms(void) {
    int signalType;
    signalType = 0;
    function(signalType);
}

void task_20ms(void) {
    int signalType;
    signalType = 1;
    function(signalType);
}

void task_50ms(void) {
    int signalType;
    signalType = 2;
    function(signalType);
}

#endif

In this example, var correctly appears as an non-shared variable if you specify the following options:

Option	Value
Configure multitasking manually
Tasks	task_10ms task_20ms task_50ms
Preprocessor definitions (-D)	POLYSPACE

However, the message on the variable shows that it can be potentially written or read by one of the tasks task_10ms, task_20ms, or task_50ms.

var is not a shared variable at all since it is accessed only in the task, task_10ms. However, the analysis reports all three tasks as accessing the variable because of an approximation on the line:

FuncPtrArray[uiSignalType].pFuncPtr();

As a result of this approximation, the analysis considers that the tasks task_10ms, task_20ms and task_50ms can potentially call each of the functions Write_to_var, No_write_read_1 and No_write_read_2. A different analysis route determines correctly that the variable is not shared.

Code Prover does not detect shared memory regions that do not have a name. Unnamed memory regions can be created by assigning absolute addresses to pointers or dynamically allocating memory. There is no named variable that represents these regions.

For instance, in this example, ptr points to dynamically allocated memory.

#include <stdlib.h>

int* ptr;

void flip() {
   *ptr = 0;
}

void flop() {
   if (*ptr == 0) {
      *ptr = 1;
  }
}
void main() {
   ptr = (int*) malloc(sizeof(int));
}