Значения летучих переменных могут меняться без явных операций записи.
Для локальных летучих переменных:
Polyspace® принимает, что переменная имеет полную область значений значений, разрешенных ее типом.
Если вы явным образом не инициализируете переменную, когда вы читаете переменную, Polyspace производит оранжевую проверку Non-initialized local variable.
В этом примере Polyspace принимает, что val1 потенциально неинициализирован, но val2 инициализируется. Polyspace считает, что + операция может вызвать переполнение, поскольку она принимает обе переменные, чтобы иметь все возможные значения, разрешенные их типами данных.
int func (void)
{
volatile int val1, val2=0;
return( val1 + val2);
}Для глобальных изменчивых переменных:
Polyspace принимает, что переменная имеет полную область значений значений, разрешенных ее типом.
Можно ограничивать область значений внешне. См. «Ограничение глобальной переменной Области значений».
Даже если вы явным образом не инициализируете переменную, когда вы читаете переменную, Polyspace производит зеленую проверку Non-initialized variable.
Если первопричиной проверки оранжевого цвета является локальная переменная volatile, вы не можете переопределить допущения по умолчанию и ограничить значения переменных volatile. Попробуйте одно из следующих:
Если изменчивая переменная представляет аппаратные данные, смотрите, можно ли использовать вызов функции для моделирования этого извлечения данных. Для примера замените volatile int port_A с int port_A = read_location(). Вы не должны определять функцию. Polyspace заглушает неопределенные функции. Затем можно задать ограничения на возвращаемые функцией значения с помощью опции Constraint setup (-data-range-specifications).
Посмотрите, можно ли скопировать содержимое летучей переменной в глобальную энергонезависимую переменную. Затем можно ограничить значения глобальных переменных по всему коду. См. «Ограничение глобальной переменной Области значений».
Замените переменную volatile на упорную функцию, но только для верификации. Перед верификацией задайте ограничения на упрямые функции.
Напишите скрипт Perl, который заменяет каждое объявление переменной с энергонезависимым объявлением, где вы получаете значение переменных из вызова функции.
Для примера, если ваш код содержит линию volatile s8 PORT_A, ваш скрипт Perl может содержать эту замену:
$line=~ s/^\s*volatile\s*s8\s*PORT_A;/s8 PORT_A = random_s8();/g;
Укажите местоположение этого скрипта Perl для опции анализа Command/script to apply to preprocessed files (-post-preprocessing-command).
В файле включения предоставьте объявление функции. Для примера, для функции random_s8Файл включения может содержать следующее объявление:
#ifndef POLYSPACE_H #define POLYSPACE_H signed char random_s8(void); #endif
Вставка #include директива для вашего файла включения в соответствующие исходные файлы
Вместо ручной вставки укажите расположение файла include для опции анализа Include (-include).