Exponenta Banner

Уважайте типы в полях (-respect-types-in-fields)

Не бросайте неуказательные поля структуры к указателям

Описание

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

Укажите, что поля структуры, не объявленные первоначально как указатели, не будут брошены к указателям позже.

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

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Verification Assumptions.

Командная строка: Используйте опцию -respect-types-in-fields. Смотрите информацию о Командной строке.

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

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

Настройки

На

Верификация принимает, что поля структуры, не объявленные первоначально как указатели, не будут брошены к указателям позже.

Код с опцией прочьКод с опцией на
struct {
    unsigned int x1;
    unsigned int x2;
} S;

void funct(void) {
    int var, *tmp;
    S.x1 = &var;     
    tmp = (int*)S.x1;
    *tmp = 1;                     
    assert(var==1);
}

В этом примере поля S объявляются как целые числа, но S.x1 брошен к указателю. С выключенной опцией Polyspace® разрешает бросок.

struct {
    unsigned int x1;
    unsigned int x2;
} S;

void funct(void) {
    int var, *tmp;
    S.x1 = &var;     
    tmp = (int*)S.x1;
    *tmp = 1;                     
    assert(var==1);
}

В этом примере поля S объявляются как целые числа, но S.x1 брошен к указателю. С включенной опцией Polyspace игнорирует бросок. Поэтому это игнорирует инициализацию var через указатель (int*)S.x1 и производит красную ошибку Non-initialized local variable, когда var читается.

От (значения по умолчанию)

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

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

Параметр: -respect-types-in-fields
Значение по умолчанию: 'off'
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -respect-types-in-fields
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -respect-types-in-fields

Смотрите также

|

Темы

Документация Polyspace Code Prover
Поддержка