CBMC
Loading...
Searching...
No Matches
may_be_same_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: May Be Same Object
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "may_be_same_object.h"
13
14#include <util/pointer_expr.h>
16
17#include "may_alias.h"
18
20{
21 if(src.id() == ID_element_address)
23 else if(src.id() == ID_field_address)
25 else
26 return src;
27}
28
30 const exprt &a,
31 const exprt &b,
32 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
33 const namespacet &ns)
34{
37
39 return true_exprt();
40 else if(
43 return false_exprt();
44
46 return false_exprt();
47
49 return false_exprt();
50
51 return ::same_object(a_stripped, b_stripped);
52}
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3200
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The Boolean constant true.
Definition std_expr.h:3191
bool stack_and_not_dirty(const exprt &expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
May Alias.
exprt strip_member_element(const exprt &src)
exprt may_be_same_object(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
May Be Same Object.
API to expression classes for Pointers.
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Various predicates over pointers in programs.