cprover
std_code.cpp File Reference
#include "std_code.h"
#include "std_expr.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. More...
 

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
conditioncondition to assert
source_locationsource 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 111 of file std_code.cpp.

References exprt::add_source_location(), exprt::copy_to_operands(), loc, and exprt::operands().

Referenced by java_bytecode_instrumentt::check_arithmetic_exception(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), java_bytecode_instrumentt::check_class_cast(), and java_bytecode_instrumentt::check_null_dereference().