#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. Поликосмическая Ошибка контролер утверждения Finder™ не сигнализирует утверждения с постоянным нулевым параметром, assert(0). Эти типы утверждений обычно используются в качестве динамических проверок во время выполнения. Путем вставки assert(0), вы указываете, что программа не должна достичь этого оператора во время выполнения, в противном случае происходит сбой программы.

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