-permissive-function-pointer)Позвольте несоответствие типов между указателями функции и функциями, на которые они указывают
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что верификация должна позволить вызовы указателя функции, где тип указателя функции не совпадает с типом функции.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Check Behavior. Смотрите Зависимость для других опций, которые необходимо также включить.
Командная строка и файл опций: Используйте опцию -permissive-function-pointer. Смотрите информацию о командной строке.
По умолчанию Программа автоматического доказательства Кода не распознает вызовы через указатели функции, когда несоответствие типов происходит. Зафиксируйте несоответствие типов, когда это возможно.
Используйте эту опцию если:
Вы не можете зафиксировать несоответствие типов, и
Анализ не покрывает значительный фрагмент вашего кода, потому что вызовы через указатели функции не распознаны.
Верификация должна позволить вызовы указателя функции, где тип указателя функции не совпадает с типом функции. Например, функция, объявленная как int f(int*) может быть вызван указателем функции, объявленным как int (*fptr)(void*).
Только несоответствия типов между типами указателей позволены. Несоответствия типов между неуказательными типами вызывают ошибки компиляции. Например, функция, объявленная как int f(int) не может быть вызван указателем функции, объявленным как int (*fptr)(double).
Верификация должна потребовать, чтобы аргумент и возвратил типы указателя функции и функции, которую это вызывает, идентичны.
Несоответствия типов обнаруживаются с проверкой Correctness condition.
С источниками, которые используют указатели функции экстенсивно, включая эту опцию, может вызвать потерю в эффективности. Эта потеря происходит, потому что верификация должна рассмотреть больше путей к выполнению.
Используя эту опцию может увеличить число оранжевых проверок. Некоторые из этих оранжевых проверок могут показать действительную проблему с кодом.
Рассмотрите эти примеры, где несоответствие типов находится между типом указателя функции и функцией, на которую это указывает:
В этом примере, указатель функции 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 проверка появляется на вызове 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 проверка появляется на вызове obj_fptr(&pt) и функциональный foo не проверяется. Если вы используете эту опцию, функция содержит оранжевую проверку на strlen вызвать. Рассмотрите проверку тщательно и убедитесь, что несоответствие типов не вызывает проблемы.
Эта опция доступна, только если вы устанавливаете Source code language (-lang) toc.
Параметр: -permissive-function-pointer |
| Значение по умолчанию: Off |
Пример (Программа автоматического доказательства Кода):
Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |