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

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

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

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

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

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

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

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

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

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

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

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

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

int*** stub(void);

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