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