Переменные диапазоны в подсказках исходного кода после анализа Code Prover

Polyspace^® Code Prover™ анализирует код C/C++ для ошибок времени выполнения и сообщает о результатах анализа, как проверяет операции. Проверки окрашены в зеленый, красный цвет, или оранжевые на основе того, передают ли они, перестали работать или остаются неокончательными. В дополнение к проверкам анализ также сообщает об областях значений относительно переменных в подсказках в исходном коде. Эти подсказки области значений могут поддержать расследование проверок на этапе выполнения, о которых сообщают, и также упростить более глубокое понимание кода, когда используется с другими инструментами навигации в пользовательском интерфейсе Polyspace или Polyspace доступ к веб-интерфейсу.

Например, эта подсказка на переменной beta указывает, что переменная является локальной переменной, имеет тип данных float (на цели, где float имеет 32 бита), и имеет значение в области значений [0.1.. 0.5]. Область значений комбинирует значения beta от всех возможных путей к выполнению, которые проходят через ту операцию кода.

Почему области значений отчетов Code Prover на переменных

Code Prover анализирует каждую операцию в исходном коде для всех возможных путей к выполнению посредством операции (удовлетворяющий предположениям верификации). Когда анализ сообщает об области значений относительно экземпляра переменной или операции, значений объединений диапазона от всех путей к выполнению, которые приводят к переменной или операции.

Рассмотрите следующий пример. Когда Code Prover анализирует функциональный func, анализ сообщает о переменных диапазонах почти относительно всех переменных в функции. Комментарии к коду на каждой линии показывают переменные диапазоны, о которых сообщают в анализе Code Prover. Обратите внимание на то, что показанные области значений являются теми, которые происходят после операций на линии.

int func(unsigned int count) { // count is in [0 .. UINT_MAX]
    int var;
    if(count <= 5)
        var = count; //var is in [0..5]
    else
        var = 100;
    return var; //var is 100 or in [0..5]
}

Например, вы видите переменные диапазоны в подсказках:

В начале функции.
Предположим тот func не называется в другом месте в коде. На основе типа данных unsigned int, Code Prover принимает тот count может иметь значения в области значений [0.. 2³² - 1] или [0.. UINT_MAX].
В каждой ветви условного оператора.
Путь к выполнению может ввести if ветвь if-else оператор, только если count меньше чем или равно 5. Поэтому в if блок, count может иметь значения только в области значений [0.. 5]. Переменная var, который получает его значение от ограниченного count, также имеет то же ограничение.
В конце, когда функция возвращается.
В return оператор, var может иметь любого значение [0.. 5] от if перейдите или значение 100 от else ветвь. Подсказка на var в return оператор объединяет эти две области значений и показывает область значений, 100 или [0.. 5].

Используя подсказки на переменных диапазонах, можно отследить поток данных в коде и изучить, как переменная получает значение, которое могло привести к ошибке времени выполнения.

Почему переменные диапазоны могут иногда быть более узкими, чем ожидалось

Иногда, область значений, о которой сообщают относительно переменной, может быть более узкой, чем, что вы ожидаете. Более узкая, чем ожидалось область значений может означать, что две на вид несвязанных переменные могут быть связаны от предыдущей операции.

Рассмотрите этот пример. Комментарии к коду на каждой линии показывают переменные диапазоны, о которых сообщают в анализе Code Prover в конце операций на линии.

void func(int arg) {

    int first, second, diff;
    first = arg;
    assert( first >= 0 && first <= 256*400); // first is in [0 .. 102400]
    second = (first << 4);  // second is in [0 .. 1638400]
    diff = (first * 16) -  (second + 256);  // diff is only -256
}

На первый взгляд, подсказка на diff в последней линии может быть удивительным. Переменная first находится в области значений [0.. 102400] и переменная second находится в области значений [0.. 1638400], но различие diff имеет только одно значение, -256.

Причина одного значения diff это предыдущая операция:

second = (first << 4);

связывает first и second таким способом, который first * 16 всегда равно second, независимо от значений first и second. Поэтому они отменяют друг друга на всех путях к выполнению, ведя к одному значению diff.

Если вы видите более узкие, чем ожидалось области значений в своем коде, ищете предыдущие операции, которые могут связать две из переменных, вовлеченных в текущую операцию. Можно также ввести прагму Inspection_Point перед операцией и затем анализируют код, чтобы идентифицировать отношение между двумя из переменных в операции. Смотрите Находят Отношения Между Переменными в Коде.

Документация