Invalid parameter of stubbed function

Parameter of a stubbed function is not valid

expand all in page

Description

This check determines if arguments passed to a stubbed function matches its parameters. Polyspace® creates expectation for the passed arguments based on the prototype of the stubbed function and if the expectations are not met, this check is reported.

Polyspace checks the parameter of a stubbed function if the parameter satisfies these criteria:

  • Parameter is not a pointer to void (void*).

  • Parameter is not a pointer to a function.

  • Parameter is not a pointer to a structure the definition of which is not available to the analysis.

For checked pointer parameters, Polyspace checks if the pointer is a null pointer. If the pointer is not null, Polyspace checks if it is allocated with sufficient memory to accommodate the pointed type. Additionally, if the pointed object is const-qualified, Polyspace checks if the pointed memory is initialized.

For checked array parameter with length N and type T, Polyspace checks that the first element of the array points to a valid location and that N elements of type T can be dereferenced. Additionally, if the array is a const array, Polyspace checks if the array elements are initialized.

This check is reported only if you specify the option -check-parameter-of-stubbed-functions.

Diagnosing This Check

To diagnose this check, read the message on the Result Details pane. The message shows the expected argument and the actual argument that causes a result:

results details showing expected and actual values of input and output

To investigate the root cause of the issue further, verify that the argument passed to the reported function matches the parameter of the stubbed function.

Examples

expand all

In this code, the prototype of the extern function FuncA is provided to the Polyspace Code Prover™ analysis. Even though the definition of the function is not available, Polyspace expects that this function accepts valid pointers to MyStruct objects. 

#include <stddef.h>
#include <stdlib.h>

struct MyStruct {
    char chars[10];
    int nums[5];
};

extern void FuncA(struct MyStruct *ptr);
extern void FuncB(const struct MyStruct *ptr);

void call_funcA() {
    struct MyStruct obj;
    FuncA(&obj);
    int value;
    FuncA(&value);
}

void call_funcB() {
    const struct MyStruct *ptr = (const struct MyStruct *)malloc(sizeof(struct MyStruct));
    ptr->nums[0] = 3;
    FuncB(ptr);// Orange
}

  • The call FuncA(&obj) meets the expectation because obj is an object of MyStruct type. Polyspace reports a green check.

  • The call FuncA(&value) fails the expectation because the variable value is an integer. Polyspace reports a red check.

  • The call FuncB(&ptr) fails the expectation because Polyspace cannot verify that the memory pointed to py ptr is initialized. Polyspace reports an orange check.

In this example, the prototype of the extern function func states that the function expects a const integer array with 2 elements. Polyspace reports a green runtime check when the function func is called with an array of two elements, each of which must be initialized.

extern void func(const int[2]);
volatile int val;

int main(){
    if (val) {
        int arr1[2] = {0, 0};
        func(arr1); //Green STUB_PRECONDITION
    }
    if (val) {
        int arr2 = 0;
        func(arr2); //red STUB_PRECONDITION -- Not an array
    }
    if (val) {
        int arr3[2];
        func(arr3); //red STUB_PRECONDITION -- not initialized
    }
    if (val) {
        int arr4[2];
        arr4[0] = 0;
        func(arr4); //orange STUB_PRECONDITION -- partially initialized
    }
}

  • The call func(arr1) meets the expectation because arr1 is an array with two initialized elements. Polyspace reports a green check.

  • The call func(arr2) fails the expectation because the variable arr2 is an integer. Polyspace reports a red check.

  • The call func(arr3) fails the expectation because the elements of arr3 are not initialized. Polyspace reports a red check.

  • The call func(arr4) fails the expectation because only one of the elements of arr3 is initialized. Polyspace reports an orange check.

Check Information

Group: Other
Language: C|C++
Acronym: stub_precondition

See Also

| | | | | |

Topics