Exponenta Banner
exponenta event banner

Respect types in fields (-respect-types-in-fields)

Не приводите неуказательные поля структуры к указателям

Описание

Эта опция влияет только на анализ Code Prover.

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

Задать опцию

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

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

Зачем использовать эту опцию

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

Настройки

На

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

Код с отключенной опциейКод с опцией on
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 считывается.

Off (по умолчанию)

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

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

Параметр: -respect-types-in-fields
По умолчанию: Off
Пример (Code Prover): Polyspace Code Prover -sources file_name -respect-types-in-fields
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -respect-types-in-fields

См. также

|

Темы

Документация Polyspace Code Prover

Поддержка