Разрешающий указатель функции вызывает (-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) на C.

Информация о командной строке

Параметр: -permissive-function-pointer
Значение по умолчанию: 'off'
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -lang c -permissive-function-pointer
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -lang c -permissive-function-pointer