Значения энергозависимых переменных могут измениться без явных операций записи.
Для локальных энергозависимых переменных:
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 int port_A с int port_A = read_location(). Вы не должны задавать функцию. Polyspace блокирует неопределенные функции. Можно затем задать ограничения на функциональные возвращаемые значения с помощью опции 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).