Respect types in fields (`-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` читается.

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 - источники file_name - уважайте типы в полях

Пример (Сервер Программы автоматического доказательства Кода):

сервер программы автоматического доказательства полипробела кода - источники file_name - уважайте типы в полях

Темы

Задайте аналитические опции Polyspace

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

Поддержка

Памятка переводчика

1. Если смысл перевода понятен, то лучше оставьте как есть и не придирайтесь к словам, синонимам и тому подобному. О вкусах не спорим.

2. Не дополняйте перевод комментариями “от себя”. В исправлении не должно появляться дополнительных смыслов и комментариев, отсутствующих в оригинале. Такие правки не получится интегрировать в алгоритме автоматического перевода.

3. Сохраняйте структуру оригинального текста - например, не разбивайте одно предложение на два.

4. Не имеет смысла однотипное исправление перевода какого-то термина во всех предложениях. Исправляйте только в одном месте. Когда Вашу правку одобрят, это исправление будет алгоритмически распространено и на другие части документации.

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

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

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