-check-parameter-of-stubbed-functions

Enable checking pointer parameters of stubbed functions

Syntax

-check-parameter-of-stubbed-functions


Description

This option affects a Code Prover analysis only.

-check-parameter-of-stubbed-functions enables the runtime check Invalid parameter of stubbed function.

By default, Polyspace^® does not check the parameters of a stubbed function. For example, consider this code where the prototype for an extern function is available but the definition is not:

struct MyStruct {
    char chars[10];
    int nums[5];
};
extern void FuncA(struct MyStruct *ptr);

When analyzing such code, Polyspace uses placeholder stubs for the extern function and assumes that the parameters are full range variables. The parameters of the prototype are not checked. if you specify this option, Polyspace checks if the parameters of a stubbed function meet 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.

If these criteria are satisfied, Polyspace checks the parameters of stubbed functions and reports the runtime check Invalid parameter of stubbed function.

If you run verification from the user interface (desktop products only), specify the option in the Other field. See Other.

Examples

In this example, the prototype of the extern function FuncA states that the function expects a pointer to objects of type MyStruct. Polyspace reports a red runtime check when the function FuncA is called with an int pointer.

#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); //green stub_precondition
	int value;
	FuncA(&value); //red stub_precondition
}

To enable the Invalid parameter of stubbed function and run this example, copy this code into the file src.c and specify these options:

 polyspace-code-prover -sources src.c  -main-generator -main-generator-calls all -check-parameter-of-stubbed-functions -lang c

In the Polyspace user interface, use the options listed in this table.

Option	Specification
Other	-check-parameter-of-stubbed-functions
Verify module or library (-main-generator)	On
Functions to call (-main-generator-calls)	all