-respect-types-in-globals)Не бросайте неуказательные глобальные переменные к указателям
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что глобальные переменные, не объявленные первоначально как указатели, не будут брошены к указателям позже.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Verification Assumptions.
Командная строка: Используйте опцию -respect-types-in-globals. Смотрите информацию о Командной строке.
Используйте эту опцию, чтобы идентифицировать и запретить броски от неуказательных глобальных переменных до указателей.
НаВерификация принимает, что глобальные переменные, не объявленные первоначально как указатели, не будут брошены к указателям позже.
От (значения по умолчанию)Верификация принимает, что глобальные переменные могут быть брошены к указателям, даже когда они не объявляются как указатели.
Если вы выбираете эту опцию, количество регистраций вашего кода может измениться. Можно использовать эту опцию и изменение в результатах идентифицировать случаи, куда вы бросаете неуказательные переменные к указателям.
Например, в следующем примере, когда вы выбираете опцию, результаты имеют тот меньше оранжевой проверки и еще одна красная проверка.
| Код с опцией прочь | Код с опцией на |
|---|---|
int global;
void main(void) {
int local;
global = (int)&local;
*(int*)global = 5;
assert(local==5);
}В этом примере | int global;
void main(void) {
int local;
global = (int)&local;
*(int*)global = 5;
assert(local==5);
}В этом примере |
Параметр: -respect-types-in-globals |
| Значение по умолчанию: 'off' |
Пример (программа автоматического доказательства кода):
|
Пример (сервер программы автоматического доказательства кода):
|