CBMC
may_alias.h File Reference

May Alias. More...

#include <util/std_expr.h>
#include <unordered_set>
+ 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< exprtmay_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 &)
 

Detailed Description

May Alias.

Definition in file may_alias.h.

Function Documentation

◆ 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.

◆ 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.