cprover
|
May Alias. More...
#include "may_alias.h"
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <util/symbol.h>
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 optionalt< 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) |
optionalt< exprt > | same_address (const exprt &a, const exprt &b, const namespacet &ns) |
optionalt< exprt > | may_alias (const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns) |
May Alias.
Definition in file may_alias.cpp.
Definition at line 138 of file may_alias.cpp.
|
static |
Definition at line 95 of file may_alias.cpp.
Definition at line 63 of file may_alias.cpp.
optionalt< 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 222 of file may_alias.cpp.
Definition at line 21 of file may_alias.cpp.
Definition at line 75 of file may_alias.cpp.
Definition at line 149 of file may_alias.cpp.
bool stack_and_not_dirty | ( | const exprt & | expr, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns ) |
Definition at line 108 of file may_alias.cpp.