Если Polyspace® не может определить значение переменных из кода, он принимает, что переменная имеет полный спектр значений, позволенных его типом.
Например, для переменной целочисленного типа, чтобы определить минимальное и позволенное максимальное значение, Polyspace использует следующие критерии:
Стандарт C указывает, что областью значений n со знаком битная переменная целочисленного типа должен быть, по крайней мере, [-(2n-1-1), 2n-1-1]
Target processor type, который вы задаете, определяет количество битов, выделенных для определенного типа. Для получения дополнительной информации смотрите Target processor type (-target).
Polyspace принимает, что ваша цель использует дополнительное представление two для целых чисел со знаком. Программное обеспечение использует это представление, чтобы определить точную область значений переменной. В этом представлении области значений n со знаком битной переменной целочисленного типа является [-2n-1, 2n-1-1]
Например, для процессора i386:
Переменная char имеет 8 битов. Стандарт C указывает, что область значений переменной char должна быть [по крайней мере-127 127].
Используя дополнительное представление two, Polyspace принимает, что точная область значений переменной char [-128 127].
Чтобы определить область значений, которую Polyspace принимает для определенного типа:
Запустите верификацию на этом коде. Замените type на имя типа, такое как int.
type getVal(void);
void main() {
type val = getVal();
}Откройте свои результаты верификации. На панели Source установите свой курсор на val.
Подсказка предоставляет спектр, который Polyspace принимает для type. Поскольку getVal не задан, Polyspace принимает, что возвращаемому значению getVal позволил полный спектр значений type.