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

Позвольте несоответствие типов между указателями функции и функциями, на которые они указывают

Описание

Эта опция влияет на анализ Code Prover только.

Укажите, что верификация должна позволить вызовы указателя функции, где тип указателя функции не совпадает с типом функции.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Check Behavior. Смотрите Зависимость для других опций, которые необходимо также включить.

Командная строка и файл опций: Используйте опцию -permissive-function-pointer. Смотрите информацию о командной строке.

Почему использование эта опция

По умолчанию Code Prover не распознает вызовы через указатели функции, когда несоответствие типов происходит. Зафиксируйте несоответствие типов, когда это возможно.

Используйте эту опцию если:

  • Вы не можете зафиксировать несоответствие типов, и

  • Анализ не покрывает значительный фрагмент вашего кода, потому что вызовы через указатели функции не распознаны.

Настройки

On

Верификация должна позволить вызовы указателя функции, где тип указателя функции не совпадает с типом функции. Например, функция, объявленная как 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) ;
      }

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

Зависимость

Эта опция доступна, только если вы устанавливаете Source code language (-lang) toc.

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

Параметр: -permissive-function-pointer
Значение по умолчанию: Off
Пример (Code Prover): Polyspace Code Prover - источники file_name - Ленг c - разрешающий указатель функции
Пример (Сервер Code Prover): сервер программы автоматического доказательства полипробела кода - источники file_name - Ленг c - разрешающий указатель функции