CBMC
Loading...
Searching...
No Matches
may_alias.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Solver
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_CPROVER_MAY_ALIAS_H
13#define CPROVER_CPROVER_MAY_ALIAS_H
14
15#include <util/std_expr.h> // IWYU pragma: keep
16
17#include <unordered_set>
18
19class namespacet;
20
21bool is_object_field_element(const exprt &);
22
23// check whether the given two addresses may be aliases
24std::optional<exprt> may_alias(
25 const exprt &,
26 const exprt &,
27 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
28 const namespacet &);
29
31 const exprt &,
32 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
33 const namespacet &);
34
35#endif // CPROVER_CPROVER_MAY_ALIAS_H
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Base class for all expressions.
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool is_object_field_element(const exprt &)
Definition may_alias.cpp:62
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 &)
API to expression classes.