CBMC
may_be_same_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: May Be Same Object
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPROVER_MAY_BE_SAME_OBJECT_H
13 #define CPROVER_CPROVER_MAY_BE_SAME_OBJECT_H
14 
15 #include <util/std_expr.h> // IWYU pragma: keep
16 
17 #include <unordered_set>
18 
19 class namespacet;
20 
21 // check whether the given two addresses may point to same object
22 exprt may_be_same_object(
23  const exprt &,
24  const exprt &,
25  const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
26  const namespacet &);
27 
28 #endif // CPROVER_CPROVER_MAY_BE_SAME_OBJECT_H
address_taken
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Definition: address_taken.cpp:51
exprt
Base class for all expressions.
Definition: expr.h:56
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
may_be_same_object
exprt may_be_same_object(const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
Definition: may_be_same_object.cpp:29
std_expr.h
API to expression classes.