В этом примере, указатель функции obj_fptr имеет аргумент, который является указателем на трехэлементный массив. Однако это указывает на функцию, соответствующий аргумент которой является указателем на четырехэлементный массив. В теле foo, четыре элемента массива читаются и постепенно увеличиваются. Четвертый элемент не существует и ++ операция читает бессмысленное значение.

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)++;
    }
}

Без этой опции, оранжевого Correctness condition (Polyspace Code Prover Access) проверка появляется на вызове obj_fptr(&ptr) и функциональный foo не проверяется. Если вы используете эту опцию, тело foo содержит несколько оранжевых проверок. Рассмотрите проверки тщательно и убедитесь, что несоответствие типов не вызывает проблемы.

В этом примере указатель функции имеет аргумент, который является указателем на структуру с тремя float члены. Однако соответствующий аргумент функции является указателем на несвязанную структуру с одним членом массивов. В теле функции, strlen функция используется, принимая член массивов. Вместо этого strlen вызовите читает float члены и могут считать бессмысленные значения, например, значения, сохраненные в дополнении структуры.

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

Без этой опции, оранжевого Correctness condition (Polyspace Code Prover Access) проверка появляется на вызове obj_fptr(&pt) и функциональный foo не проверяется. Если вы используете эту опцию, функция содержит оранжевую проверку на strlen вызвать. Рассмотрите проверку тщательно и убедитесь, что несоответствие типов не вызывает проблемы.