CBMC
Loading...
Searching...
No Matches
Functions
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< 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 &)
 

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.

AltStyle によって変換されたページ (->オリジナル) /