sentinel_dll.cpp File Reference

Axioms. More...

#include "sentinel_dll.h"
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include "state.h"

Include dependency graph for sentinel_dll.cpp:

Go to the source code of this file.

Functions
std::optional< exprt >	sentinel_dll_member (const exprt &state, const exprt &node, bool next, const namespacet &ns)
std::optional< exprt >	sentinel_dll_next (const exprt &state, const exprt &node, const namespacet &ns)
std::optional< exprt >	sentinel_dll_prev (const exprt &state, const exprt &node, const namespacet &ns)

Detailed Description

Axioms.

Definition in file sentinel_dll.cpp.

Function Documentation

sentinel_dll_member()

std::optional<exprt> sentinel_dll_member	(	const exprt &	state,
		const exprt &	node,
		bool	next,
		const namespacet &	ns
	)

Definition at line 20 of file sentinel_dll.cpp.

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.