Включите адресную арифметику с указателями через поля (-allow-ptr-arith-on-struct)

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

Описание

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

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

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

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

Командная строка: Используйте опцию -allow-ptr-arith-on-struct. Смотрите информацию о Командной строке.

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

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

Настройки

На

Указатель, присвоенный полю структуры, может указать вне границ, наложенных полем, пока это указывает в структуре. Например, в следующем коде, если вы не используете эту опцию, верификация произведет красную проверку Illegally dereferenced pointer:

void main(void) {
struct S {char a; char b; int c;} x;
char *ptr = &x.b;
ptr ++;
*ptr = 1; // Red on the dereference, because ptr points outside x.b
}
От (значения по умолчанию)

Указатель, присвоенный полю структуры, может указать только в границах, наложенных полем.

Советы

  • Верификация не позволяет указатель с отрицательными значениями смещения. Это поведение происходит независимо от того, выбираете ли вы опцию Enable pointer arithmetic across fields.

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

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

  • Перед использованием этой опции рассмотрите затраты на использование адресной арифметики с указателями через различные поля структуры.

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

Зависимость

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

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

Параметр: -allow-ptr-arith-on-struct
Значение по умолчанию: 'off'
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -allow-ptr-arith-on-struct
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -allow-ptr-arith-on-struct