-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) toc.
Параметр: -allow-ptr-arith-on-struct |
| Значение по умолчанию: 'off' |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |