-detect-pointer-escape)Найдите случаи, куда функция возвращает указатель на одну из его локальных переменных
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что верификация должна обнаружить случаи, где вы получаете доступ к переменной вне ее осциллографа через указатели. Такой доступ может произойти, например, когда функция возвращает указатель на локальную переменную, и вы разыменовываете указатель вне функции. Неопределенное поведение разыменовать причин, потому что локальная переменная, на которую указывает указатель, не живет вне функции.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Check Behavior.
Командная строка: Используйте опцию -detect-pointer-escape. Смотрите информацию о командной строке.
Используйте эту опцию, чтобы включить обнаружение Escape указателя.
OnПроверка Illegally dereferenced pointer выполняет дополнительную задачу помимо ее обычных технических требований. Когда вы разыменовываете указатель, проверка также определяет, получаете ли вы доступ к переменной вне ее осциллографа через указатель. Проверка:
Красный, если ко всем переменным, на которые указывает указатель, получают доступ вне их осциллографа.
Например, вы разыменовываете указатель ptr в функциональном func это называется дважды в вашем коде. В обоих вызовах, когда вы выполняете разыменовать *ptr, ptr указывает на переменные вне их осциллографа. Поэтому проверка Illegally dereferenced pointer является красной.
Оранжевый, если к только некоторым переменным, на которые указывает указатель, получают доступ вне их осциллографа.
Зеленый, если ни к одной из переменных, на которые указывает указатель, не получают доступ вне их осциллографа и других требований проверки, также удовлетворены.
В следующем коде, если вы включаете эту опцию, Polyspace® Code Prover™ производит красный Illegally dereferenced pointer, проверяют *ptr. В противном случае, Illegally dereferenced pointer проверяют *ptr является зеленым.
void func2(int *ptr) {
*ptr = 0;
}
int* func1(void) {
int ret = 0;
return &ret ;
}
void main(void) {
int* ptr = func1() ;
func2(ptr) ;
}
ret получен доступ вне его осциллографа.
От (значения по умолчанию) Когда вы разыменовываете указатель, проверка Illegally dereferenced pointer не проверяет на то, получаете ли вы доступ к переменной вне ее осциллографа. Проверка является зеленой, даже если указатель разыменовывает, находится вне переменной scope, пока это удовлетворяет этим требованиям:
Указатель не является ПУСТЫМ.
Указатель указывает в буфере памяти.
Обнаружение уважения указателя вершины стека вне осциллографа не применяется к определенным типам указателей. Для определенных ограничений смотрите Ограничения Верификации Polyspace.
Параметр: -detect-pointer-escape |
| Значение по умолчанию: Off |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники |