sentinel_dll.h File Reference

#include <util/std_expr.h>

Include dependency graph for sentinel_dll.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	state_is_sentinel_dll_exprt

Functions
const state_is_sentinel_dll_exprt &	to_state_is_sentinel_dll_expr (const exprt &expr)
	Cast an exprt to a state_is_sentinel_dll_exprt.
state_is_sentinel_dll_exprt &	to_state_is_sentinel_dll_expr (exprt &expr)
	Cast an exprt to a state_is_sentinel_dll_exprt.
std::optional< exprt >	sentinel_dll_next (const exprt &state, const exprt &node, const namespacet &)
std::optional< exprt >	sentinel_dll_prev (const exprt &state, const exprt &node, const namespacet &)

Function Documentation

sentinel_dll_next()

std::optional< exprt > sentinel_dll_next	(	const exprt &	state,
		const exprt &	node,
		const namespacet &	ns
	)

Definition at line 73 of file sentinel_dll.cpp.

sentinel_dll_prev()

std::optional< exprt > sentinel_dll_prev	(	const exprt &	state,
		const exprt &	node,
		const namespacet &	ns
	)

Definition at line 79 of file sentinel_dll.cpp.

to_state_is_sentinel_dll_expr() [1/2]

const state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr ( const exprt &  expr )

inline

Cast an exprt to a state_is_sentinel_dll_exprt.

expr must be known to be state_is_sentinel_dll_exprt.

Parameters

expr	Source expression

Returns

Object of type state_is_sentinel_dll_exprt

Definition at line 85 of file sentinel_dll.h.

to_state_is_sentinel_dll_expr() [2/2]

state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr ( exprt &  expr )

inline

Cast an exprt to a state_is_sentinel_dll_exprt.

expr must be known to be state_is_sentinel_dll_exprt.

Parameters

expr	Source expression

Returns

Object of type state_is_sentinel_dll_exprt

Definition at line 95 of file sentinel_dll.h.