#include <assert.h>

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

В этом примере assert функция проверяет, является ли входная переменная, theta, меньше или равно нулю. Утверждение прекращает работать из-за theta является беззнаковым целым числом, поэтому значение в начале функции как минимум равняется нулю. The += оператор увеличивает это положительное значение на пять. Поэтому область значений 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), вы указываете, что программа не должна достигать этого оператора во время исполнения, в противном случае происходит сбой программы.

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