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

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

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

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

  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.

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

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

Например, все дереференции считаются действительными в этом коде:

int*** stub(void);

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