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

 Различие между уровнем 0 и 1

#include <stdlib.h>

void ratio    (float x, float *y)
{
    *y=(abs(x-*y))/(x+*y);
}

void level1 (float x,
                float y, float *t)
{ float v;
    v = y;
    ratio (x, &y);
    *t = 1.0/(v - 2.0 * x);
}

float level2(float v)
{
    float t;
    t = v;
    level1(0.0, 1.0, &t);
    return t;
}

void main(void)
{
    float r,d;
    d= level2(1.0);
    r = 1.0 / (2.0 - d);
}

#include <stdlib.h>

void ratio    (float x, float *y)
{
    *y=(abs(x-*y))/(x+*y);
}

void level1 (float x,
                float y, float *t)
{ float v;
    v = y;
    ratio (x, &y);
    *t = 1.0/(v - 2.0 * x);
}

float level2(float v)
{
    float t;
    t = v;
    level1(0.0, 1.0, &t);
    return t;
}

void main(void)
{
    float r,d;
    d= level2(1.0);
    r = 1.0 / (2.0 - d);
}

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

Для лучших результатов используйте опцию Software Safety Analysis level 2. Если верификация занимает слишком много времени, используйте более низкий Verification level. Зафиксируйте красные ошибки и код Грея прежде, чем повторно выполнить верификацию с более высокими уровнями верификации.

Используйте опцию Other экономно, поскольку это может увеличить время верификации неблагоразумной суммой. Используя Software Safety Analysis level 2 обеспечивает оптимальную верификацию вашего кода в большинстве случаев.

Если Verification Level установлен в Source Compliance Checking, не запускайте верификацию на удаленном сервере. Исходная проверка соответствия или компиляция, фаза происходит на вашем локальном компьютере так или иначе. Поэтому, если вы запускаете верификацию только в конец компиляции, верификации выполнения на вашем локальном компьютере.

C проекты: c-to-il (C к фазе преобразования промежуточного языка)

Проекты C++: cpp-to-il (C++ к фазе преобразования промежуточного языка), cpp-normalize (фаза нормализации C++), cpp-link (фаза ссылки C++)