Значения изменяемых переменных могут изменяться без явных операций записи.
Для локальных изменчивых переменных:
Polyspace ® предполагает, что переменная имеет полный диапазон значений, допустимых ее типом.
Если переменная не инициализирована явным образом, при чтении переменной Полиспейс производит проверку неинициализированной локальной переменной оранжевого цвета.
В этом примере Polyspace предполагает, что val1 потенциально не инициализирован, но val2 инициализирован. Полиспейс считает, что + операция может вызвать переполнение, поскольку она предполагает, что обе переменные имеют все возможные значения, разрешенные их типами данных.
int func (void)
{
volatile int val1, val2=0;
return( val1 + val2);
}Для глобальных изменчивых переменных:
В Polyspace предполагается, что переменная имеет полный диапазон значений, допустимых ее типом.
Диапазон можно ограничить снаружи. См. раздел Ограничение диапазона глобальных переменных.
Даже если переменная не инициализирована явным образом, при чтении переменной Полиспейс производит зеленую проверку неинициализированной переменной.
Если основной причиной проверки оранжевого цвета является локальная переменная, нельзя переопределить предположения по умолчанию и ограничить значения переменных. Попробуйте выполнить одно из следующих действий:
Если изменчивая переменная представляет аппаратные данные, проверьте, можно ли использовать вызов функции для моделирования этого извлечения данных. Например, заменить volatile int port_A с int port_A = read_location(). Определение функции не требуется. Полиспейс блокирует неопределенные функции. Затем можно задать ограничения для возвращаемых функций с помощью опции Constraint setup (-data-range-specifications).
Проверьте, можно ли скопировать содержимое энергонезависимой переменной в глобальную энергонезависимую переменную. Затем можно ограничить значения глобальных переменных во всем коде. См. раздел Ограничение диапазона глобальных переменных.
Замените изменчивую переменную упорной функцией, но только для проверки. Перед проверкой укажите ограничения для упорных функций.
Напишите сценарий 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).