-allow-ptr-arith-on-struct)Разрешить арифметику указателя на поле структуры так, чтобы оно указывало на другое поле
Эта опция влияет только на анализ Code Prover.
Задайте, что указатель, назначенный полю структуры, может указывать за его пределы, пока он указывает в структуре.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле 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
}
Off (по умолчанию) Указатель, назначенный полю структуры, может указывать только в пределах, установленных полем.
Эта верификация не позволяет использовать указатель с отрицательными значениями смещения. Это поведение происходит независимо от того, выберете ли вы Enable pointer arithmetic across fields опцию.
Использование этой опции может немного увеличить количество оранжевых проверок. Опция ослабляет ограничение, что указатель на поле структуры не может указывать на другие поля структуры. В обмен на ослабление этого ограничения верификация теряет точность на контуре полей в структуре и рассматривает структуру как единое целое. Ранее зеленые разыменования указателей теперь могут стать оранжевыми.
Используйте эту опцию, если вы следуете политике проверки только красных чеков и вам нужно работать с красными чеками из арифметики указателя в структуре.
Перед использованием этой опции учитывайте затраты на использование арифметики указателя через различные поля структуры.
В отличие от массива, представители структуры могут иметь различные типы данных. Для эффективного хранения структуры используют заполнение, чтобы учесть это различие. При увеличении указателя на представителя структуры можно не указывать на следующий представителя. Когда вы высмеиваете этот указатель, вы не можете полагаться на то, что вы читаете или пишете.
Эта опция доступна только при установке Source code language (-lang) на C.
Параметр: -allow-ptr-arith-on-struct |
| По умолчанию: Off |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |