exponenta event banner

Допущения о переменных диапазонах

Если Polyspace ® не может определить значение переменной из кода, предполагается, что переменная имеет полный диапазон значений, допустимых ее типом.

Например, для переменной целого типа, чтобы определить минимальное и максимальное допустимое значение, Polyspace использует следующие критерии:

  • Стандарт C указывает, что диапазон подписанного n-разрядная целочисленная переменная должна быть не менее [-(2n-1-1), 2n-1-1].

    Указанный тип целевого процессора определяет количество битов, выделенных для определенного типа. Дополнительные сведения см. в разделе Target processor type (-target).

  • Polyspace предполагает, что цель использует представление дополнения для целых чисел со знаком. Программа использует это представление для определения точного диапазона переменной. В этом представлении диапазон подписанного n-разрядная целочисленная переменная [-2n-1, 2n-1-1].

Например, для i386 процессор:

  • A char переменная имеет 8 битов. Стандарт C указывает, что диапазон char переменная должна быть не менее [-127,127].

  • Используя представление дополнения двух, Polyspace предполагает, что точный диапазон char переменная - [-128,127].

Чтобы определить диапазон, предполагаемый Полиспейсом для определенного типа:

  1. Выполните проверку этого кода. Заменить type с именем типа, таким как int.

    type getVal(void);
    void main() {
    		type val = getVal();
    }

  2. Откройте результаты проверки. На панели «Источник» установите курсор на val.

    Всплывающая подсказка предоставляет диапазон, предполагаемый Полиспейсом для type. С тех пор getVal не определен, Polyspace предполагает, что возвращаемое значение getVal имеет полный диапазон значений, допустимых type.