#include <assert.h>

void asserting_x(unsigned int theta) {
    theta =+ 5;
    assert(theta < 0);
}

В этом примере, assert функционируйте проверки если входная переменная, theta, меньше чем или равно нулю. Утверждение перестало работать потому что theta беззнаковое целое, таким образом, значение в начале функции является, по крайней мере, нулем. += оператор увеличивает это положительное значение пять. Поэтому область значений theta [5..MAX_INT]. theta всегда больше нуля.

#include <assert.h>

void asserting_x(unsigned int theta) {
    theta =+ 5;
    assert(theta > 0);
}

#include <assert.h>
#include <stdlib.h>

void asserting_x(int theta) {
    theta = -abs(theta);
    assert(theta < 0);
}

#include <assert.h>

#define FLAG 0

int main(void){
    int i_test_z = 0;
    float f_test_z = (float)i_test_z;

    assert(i_test_z);
    assert(f_test_z);
    assert(FLAG);

    return 0;
}

В этом примере Polyspace не делает флага assert(FLAG) как нарушение, потому что макрос задает FLAG как 0. Верификатор условий Polyspace Bug Finder™ не отмечает утверждения с помощью постоянного нулевого параметра, assert(0). Эти типы утверждений обычно используются в качестве динамических проверок во время времени выполнения. Путем вставки assert(0), вы указываете, что программа не должна достигать этого оператора в течение времени выполнения, в противном случае катастрофические отказы программы.

Однако верификатор условий действительно отмечает отказавшие утверждения, вызванные равным нулю значением переменных, как замечено в примере с assert(i_test_z) и assert(f_test_z).