Если для одной и той же операции выполняется несколько проверок, Code Prover выполняет их в определенном порядке. Порядок проверок важен, только если одна из проверок не зеленая. Если проверка имеет красный цвет, последующие проверки не выполняются. Если чек оранжевый, последующие проверки выполняются для уменьшенного множества значений. Для получения дополнительной информации смотрите Анализ Code Prover После красных и оранжевых проверок.
Простой пример - порядок проверок при разыменовании указателя. Code Prover сначала проверяет, инициализирован ли указатель, а затем проверяет, указывает ли указатель на допустимое место. Проверяйте Illegally dereferenced pointer выполняет проверку Non-initialized local variable.
Если один из операндов в двоичной операции является переменной с плавающей точкой, Code Prover выполняет следующие проверки операции в следующем порядке:
Invalid operation on floats: Если вы включите опцию, чтобы рассмотреть не конечные поплавки, эта проверка определяет, может ли операция привести к NaN.
Overflow: Эта проверка определяет, переполнен ли результат.
Если вы включите опцию рассматривать не конечные поплавки, эта проверка определяет, может ли операция привести к бесконечности.
Subnormal float: Если вы включите субнормальный режим обнаружения, эта проверка определяет, может ли операция привести к субнормальным значениям.
Например, предположим, что вы включите опции, чтобы запретить бесконечность, NaNs и субнормальные результаты. В этом примере операция y = x + 0; проверяется на все три проблемы. Операция выглядит красной, но состоит из трех проверок: оранжевого Invalid operation on floats, оранжевого Overflow и красного Subnormal float.
#include <float.h>
#include <assert.h>
double input();
int main() {
double x = input();
double y;
assert (x != x || x > DBL_MAX || (x > 0. && x < DBL_MIN));
y = x + 0.;
return 0;
}На + операция, x может иметь три группы значений: x является NaN, x > DBL_MAX, и x > 0. && x < DBL_MIN.
Проверки выполняются в следующем порядке:
Invalid operation on floats: Проверка оранжевая, потому что один путь выполнения считает, что x можно NaN.
Для следующих проверок этот путь не рассматривается.
Overflow: Проверка оранжевая, потому что одна группа путей выполнения считает, что x > DBL_MAX. Для этой группы путей + операция может привести к бесконечности.
Для следующей проверки эта группа путей не рассматривается.
Subnormal float: На остальных группах путей выполнения, x > 0. && x < DBL_MIN. Все значения x привести к субнормальным результатам. Поэтому эта проверка имеет красный цвет.
Сообщение на панели Result Details отражает это сокращение путей. Сообщение для проверки Subnormal float состояний (when finite) чтобы показать, что бесконечные значения были удалены из фактора.
Значения для левого и правого операндов отражают все значения перед операцией, а не уменьшенный множество значений. Поэтому левый операнд все равно показывает Inf и NaN даже при том, что эти значения не были рассмотрены для проверки.
Consider non finite floats (-allow-non-finite-floats) | Infinities (-check-infinite) | Invalid operation on floats | NaNs (-check-nan) | Overflow | Subnormal float