Loading...

Searching...

No Matches

may_alias.cpp File Reference

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.