Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe)

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

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Эта опция не доступна для кода, сгенерированного из кода MATLAB® или моделей Simulink®.

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

Указатели среды включают:

  • Глобальная переменная или extern указатели.

  • Указатели возвращены в заблокированные функции.

    Функция заблокирована, если ваш код не содержит функциональное определение, или вы заменяете функциональное определение при помощи опции Functions to stub (-functions-to-stub).

  • Параметры указателя функций, вызовы которых сгенерированы программным обеспечением.

    Вызов функции сгенерирован, если вы проверяете модуль или библиотеку и модуль, или библиотека не имеет явного вызова функции. Можно также обеспечить вызов функции, который будет сгенерирован с опцией Functions to call (-main-generator-calls).

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

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Verification Assumptions.

Командная строка: Используйте опцию -stubbed-pointers-are-unsafe. Смотрите информацию о командной строке.

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

Используйте эту опцию так, чтобы верификация сделала более консервативные предположения об указателях из внешних источников.

Если вы задаете эту опцию, верификация полагает, что указатели среды могут иметь NULL значение. Если вы читаете указатель среды, не проверяя на NULL, проверка Illegally dereferenced pointer отображает потенциальную ошибку оранжевым. Сообщение, сопоставленное с оранжевой проверкой, показывает, что указателем может быть NULL.

Настройки

On

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

От (значения по умолчанию)

Верификация полагает что указатели среды:

  • Не может иметь NULL значение.

  • Точки в позволенных границах.

Советы

  • Включите эту опцию во время фазы интегрирования. В этой фазе вы предоставляете полный код для верификации. Даже если оранжевая проверка произойдет из внешних источников, вы, вероятно, поместите меры защиты от небезопасных указателей из таких источников. Например, если вы получаете указатель из неизвестного источника, вы проверяете указатель на NULL значение.

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

  • Если вы проверяете реализацию кода AUTOSAR runnables, Программа автоматического доказательства Кода принимает что аргументы указателя к runnables и указателям, возвращенным в Rte_ функциями не является NULL. Вы не можете использовать эту опцию, чтобы изменить предположение. Смотрите Polyspace Запуска на Коде AUTOSAR с консервативными Предположениями.

  • Если вы включаете эту опцию, количество оранжевых регистраций вашего кода может увеличиться.

    Безопасные указатели средыНебезопасные указатели среды

    Проверка Illegally dereferenced pointer является зеленой. Верификация принимает тот env_ptr не является ПУСТЫМ, и любой разыменовывает, в позволенных границах. Верификация принимает, что результатом разыменовывания является полный спектр. Например, в этом случае, возвращаемое значение имеет полный спектр типа int.

      int func (int *env_ptr) {
          return *env_ptr;
      }

    Проверка Illegally dereferenced pointer является оранжевой. Верификация принимает тот env_ptr может быть NULL.

      int func (int *env_ptr) {
          return *env_ptr;
      }

    Если вы включаете эту опцию, количество серых проверок может уменьшиться.

    Безопасные указатели средыНебезопасные указатели среды

    Верификация принимает тот env_ptr не является ПУСТЫМ. if условие всегда верно и else блок недостижим.

      #include <stdlib.h>
      int func (int *env_ptr) {
          if(env_ptr!=NULL)
    	         return *env_ptr;
          else
    	         return 0;
      }

    Верификация принимает тот env_ptr может быть NULL. if условие не всегда верно и else блок может быть достижимым.

      #include <stdlib.h>
      int func (int *env_ptr) {
          if(env_ptr!=NULL)
    	         return *env_ptr;
          else
    	         return 0;
      }

  • Вместо того, чтобы рассмотреть все указатели среды как безопасные или небезопасные, можно индивидуально ограничить некоторые указатели среды. См. описание Initialize Pointer во Внешних Ограничениях для Анализа Polyspace.

    Когда вы индивидуально ограничиваете указатель, вы сначала задаете Init Mode, и затем задаете через опцию Initialize Pointer, является ли указателем Null, Not Null, или Maybe Null. В зависимости от Init Mode можно или заменить глобальную спецификацию для всех указателей среды или нет.

    • Если вы устанавливаете Init Mode указателя на INIT или PERMANENT, ваш выбор для Initialize Pointer заменяет вашу спецификацию для этой опции. Например, если вы задаете Not NULL для указателя среды ptr, верификация принимает тот ptr не является ПУСТЫМ, даже если вы указываете, что указатели среды должны быть рассмотрены небезопасными.

    • Если вы устанавливаете Init Mode на MAIN GENERATOR, верификация использует вашу спецификацию для этой опции.

      Для указателей, возвращенных в заблокированные функции, опция MAIN GENERATOR не доступно. Если вы заменяете глобальную спецификацию для такого указателя через опцию Initialize Pointer в ограничениях, вы не можете переключиться назад к глобальной спецификации, не изменяя опцию Initialize Pointer также.

  • Если вы отключаете эту опцию, верификация полагает, что это разыменовывает на всех глубинах указателя, допустимы.

    Например, все разыменовывание рассматриваются допустимыми в этом коде:

    int*** stub(void);
    
    void func2() {
            int ***ptr = stub();
            int **ptr2 = *ptr;
            int *ptr3 = *ptr2;
    }

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

Параметр: -stubbed-pointers-are-unsafe
Значение по умолчанию: Off
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники file_name - заблокированные указатели небезопасны
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - заблокированные указатели небезопасны
Введенный в R2017b