CBMC
Loading...
Searching...
No Matches
address_taken.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Address Taken
4
5Author: 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 [...:=...]
23static 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
50std::unordered_set<symbol_exprt, irep_hash>
51address_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.
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
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.
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
Definition state.h:200