|
cprover
|
May Alias. More...
Include dependency graph for may_alias.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| bool | is_object_field_element (const exprt &) |
| std::optional< exprt > | may_alias (const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &) |
| bool | stack_and_not_dirty (const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &) |
May Alias.
Definition in file may_alias.h.
| bool is_object_field_element | ( | const exprt & | expr | ) |
Definition at line 62 of file may_alias.cpp.
| 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.
| 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.