Permissive function pointer calls (-permissive-function-pointer)

Allow type mismatch between function pointers and the functions they point to

Description

This option affects a Code Prover analysis only.

Specify that the verification must allow function pointer calls where the type of the function pointer does not match the type of the function.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node. See Dependency for other options you must also enable.

Command line and options file: Use the option -permissive-function-pointer. See Command-Line Information.

Why Use This Option

By default, Code Prover does not recognize calls through function pointers when a type mismatch occurs. Fix the type mismatch whenever possible.

Use this option if:

• You cannot fix the type mismatch, and

• The analysis does not cover a significant portion of your code because calls via function pointers are not recognized.

Settings

On

The verification must allow function pointer calls where the type of the function pointer does not match the type of the function. For instance, a function declared as int f(int*) can be called by a function pointer declared as int (*fptr)(void*).

Only type mismatches between pointer types are allowed. Type mismatches between nonpointer types cause compilation errors. For instance, a function declared as int f(int) cannot be called by a function pointer declared as int (*fptr)(double).

Off (default)

The verification must require that the argument and return types of a function pointer and the function it calls are identical.

Type mismatches are detected with the check Correctness condition (Polyspace Code Prover Access).

Tips

• With sources that use function pointers extensively, enabling this option can cause loss in performance. This loss occurs because the verification has to consider more execution paths.

• Using this option can increase the number of orange checks. Some of these orange checks can reveal a real issue with the code.

  Consider these examples where a type mismatch occurs between the function pointer type and the function that it points to:

  • In this example, the function pointer obj_fptr has an argument that is a pointer to a three-element array. However, it points to a function whose corresponding argument is a pointer to a four-element array. In the body of foo, four array elements are read and incremented. The fourth element does not exist and the ++ operation reads a meaningless value.

    typedef int array_three_elements[3]; typedef void (*fptr)(array_three_elements*); typedef int array_four_elements[4]; void foo(array_four_elements*); void main() { array_three_elements arr[3] = {0,0,0}; array_three_elements *ptr; fptr obj_fptr; ptr = &arr; obj_fptr = &foo; //Call via function pointer obj_fptr(&ptr); } void foo(array_four_elements* x) { int i = 0; int *current_pos; for(i = 0; i< 4; i++) { current_pos = (*x) + i; (*current_pos)++; } }

    Without this option, an orange Correctness condition (Polyspace Code Prover Access) check appears on the call obj_fptr(&ptr) and the function foo is not verified. If you use this option, the body of foo contains several orange checks. Review the checks carefully and make sure that the type mismatch does not cause issues.

    

  • In this example, the function pointer has an argument that is a pointer to a structure with three float members. However, the corresponding function argument is a pointer to an unrelated structure with one array member. In the function body, the strlen function is used assuming the array member. Instead the strlen call reads the float members and can read meaningless values, for instance, values stored in the structure padding.

    #include <string.h> struct point { float x; float y; float z; }; struct message { char msg[10] ; }; void foo(struct message*); void main() { struct point pt = {3.14, 2048.0, -1.0} ; void (*obj_fptr)(struct point *) ; obj_fptr = &foo; //Call via function pointer obj_fptr(&pt); } void foo(struct message* x) { int y = strlen(x->msg) ; }

    Without this option, an orange Correctness condition (Polyspace Code Prover Access) check appears on the call obj_fptr(&pt) and the function foo is not verified. If you use this option, the function contains an orange check on the strlen call. Review the check carefully and make sure that the type mismatch does not cause issues.

Dependency

This option is available only if you set Source code language (-lang) to C.

Command-Line Information

Parameter: -permissive-function-pointer

Default: Off

Example (Code Prover): polyspace-code-prover -sources file_name -lang c -permissive-function-pointer

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -lang c -permissive-function-pointer