Functions

code_blockt create_fatal_assertion (const exprt &condition, const source_locationt &loc)

Create a fatal assertion, which checks a condition and then halts if it does not hold.

Detailed Description

Data structure representing different types of statements in a program.

Definition in file std_code.cpp.

Function Documentation

◆ create_fatal_assertion()

code_blockt create_fatal_assertion ( const exprt & condition,

const source_locationt & source_location

)

Create a fatal assertion, which checks a condition and then halts if it does not hold.

Equivalent to ASSERT(condition); ASSUME(condition) .

Source level assertions should probably use this, whilst checks that are normally non-fatal at runtime, such as integer overflows, should use code_assertt by itself.

Parameters: condition condition to assert

source_location source location to attach to the generated code; conventionally this should have comment and property_class fields set to indicate the nature of the assertion.

Returns: A code block that asserts a condition then aborts if it does not hold.

Definition at line 120 of file std_code.cpp.