CBMC
address_taken.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Address Taken
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #include "address_taken.h"
13 
14 #include <util/pointer_expr.h>
15 
16 #include "state.h"
17 
18 // we look for ❝x❞ that's
19 // * not the argument of ς(...), i.e., evaluate
20 // * not the argument of enter_scope_state(?, ?)
21 // * not the argument of exit_scope_state(?, ?)
22 // * not on the lhs of [...:=...]
23 static void find_objects_rec(
24  const exprt &src,
25  std::unordered_set<symbol_exprt, irep_hash> &result)
26 {
27  if(src.id() == ID_object_address)
28  result.insert(to_object_address_expr(src).object_expr());
29  else if(src.id() == ID_evaluate)
30  {
31  }
32  else if(src.id() == ID_enter_scope_state)
33  {
34  }
35  else if(src.id() == ID_exit_scope_state)
36  {
37  }
38  else if(src.id() == ID_update_state)
39  {
40  const auto &update_state_expr = to_update_state_expr(src);
41  find_objects_rec(update_state_expr.new_value(), result);
42  }
43  else
44  {
45  for(auto &op : src.operands())
46  find_objects_rec(op, result);
47  }
48 }
49 
50 std::unordered_set<symbol_exprt, irep_hash>
51 address_taken(const std::vector<exprt> &src)
52 {
53  std::unordered_set<symbol_exprt, irep_hash> result;
54 
55  for(auto &expr : src)
56  find_objects_rec(expr, result);
57 
58  return result;
59 }
static void find_objects_rec(const exprt &src, std::unordered_set< symbol_exprt, irep_hash > &result)
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Address Taken.
Base class for all expressions.
Definition: expr.h:56
operandst & operands()
Definition: expr.h:94
const irep_idt & id() const
Definition: irep.h:388
API to expression classes for Pointers.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:643
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
Definition: state.h:200