std_code.cpp File Reference

Data structure representing different types of statements in a program. More...

#include "std_code.h"
#include "arith_tools.h"

Include dependency graph for std_code.cpp:

Go to the source code of this file.

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.