May Alias. More...

#include "may_alias.h"
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <util/symbol.h>

Include dependency graph for may_alias.cpp:

Go to the source code of this file.

Functions
bool	permitted_by_strict_aliasing (const typet &a, const typet &b)

bool	is_object_field_element (const exprt &expr)

bool	prefix_of (const typet &a, const typet &b, const namespacet &ns)

static std::optional< object_address_exprt >	find_object (const exprt &expr)

bool	stack_and_not_dirty (const exprt &expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

static exprt	drop_pointer_typecasts (exprt src)

std::optional< exprt >	same_address (const exprt &a, const exprt &b, const namespacet &ns)

std::optional< exprt >	may_alias (const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

Detailed Description

May Alias.

Definition in file may_alias.cpp.

Function Documentation

◆ drop_pointer_typecasts()

static exprt drop_pointer_typecasts ( exprt src )

static

Definition at line 137 of file may_alias.cpp.

◆ find_object()

static std::optional<object_address_exprt> find_object ( const exprt & expr )

static

Definition at line 94 of file may_alias.cpp.

◆ is_object_field_element()

bool is_object_field_element ( const exprt & expr )

Definition at line 62 of file may_alias.cpp.

◆ may_alias()

std::optional<exprt> may_alias	(	const exprt &	a,
		const exprt &	b,
		const std::unordered_set< symbol_exprt, irep_hash > &	address_taken,
		const namespacet &	ns
	)

Definition at line 221 of file may_alias.cpp.

◆ permitted_by_strict_aliasing()

bool permitted_by_strict_aliasing	(	const typet &	a,
		const typet &	b
	)

Definition at line 20 of file may_alias.cpp.

◆ prefix_of()

bool prefix_of	(	const typet &	a,
		const typet &	b,
		const namespacet &	ns
	)

Definition at line 74 of file may_alias.cpp.

◆ same_address()

std::optional<exprt> same_address	(	const exprt &	a,
		const exprt &	b,
		const namespacet &	ns
	)

Definition at line 148 of file may_alias.cpp.

◆ stack_and_not_dirty()

bool stack_and_not_dirty	(	const exprt &	expr,
		const std::unordered_set< symbol_exprt, irep_hash > &	address_taken,
		const namespacet &	ns
	)

Definition at line 107 of file may_alias.cpp.

Functions