Если Polyspace® не может определить значение переменных из кода, он принимает, что переменная имеет полный спектр значений, позволенных его типом.
Например, для переменной целочисленного типа, чтобы определить минимальное и позволенное максимальное значение, Polyspace использует следующие критерии:
Стандарт C указывает что область значений n со знаком- битная переменная целочисленного типа должна быть, по крайней мере [-(2. n- 1-1), 2n-1-1]
Target processor type, который вы задаете, определяет количество битов, выделенных для определенного типа. Для получения дополнительной информации смотрите Target processor type (-target).
Polyspace принимает, что ваша цель использует дополнительное представление two для целых чисел со знаком. Программное обеспечение использует это представление, чтобы определить точную область значений переменной. В этом представлении, области значений n со знаком- битная переменная целочисленного типа [-2.n- 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.