CBMC
array_name.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Misc Utilities
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "array_name.h"
13 
14 #include "expr.h"
15 #include "namespace.h"
16 #include "ssa_expr.h"
17 #include "symbol.h"
18 
19 std::string array_name(
20  const namespacet &ns,
21  const exprt &expr)
22 {
23  if(expr.id()==ID_index)
24  {
25  return array_name(ns, to_index_expr(expr).array()) + "[]";
26  }
27  else if(is_ssa_expr(expr))
28  {
29  const symbolt &symbol=
30  ns.lookup(to_ssa_expr(expr).get_object_name());
31  return "array '" + id2string(symbol.base_name) + "'";
32  }
33  else if(expr.id()==ID_symbol)
34  {
35  const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
36  return "array '" + id2string(symbol.base_name) + "'";
37  }
38  else if(expr.id()==ID_string_constant)
39  {
40  return "string constant";
41  }
42  else if(expr.id()==ID_member)
43  {
44  const member_exprt &member_expr = to_member_expr(expr);
45 
46  return array_name(ns, member_expr.compound()) + "." +
47  id2string(member_expr.get_component_name());
48  }
49 
50  return "array";
51 }
array_name
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1478
exprt
Base class for all expressions.
Definition: expr.h:55
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
namespace.h
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2843
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:222
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:396
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2793
ssa_expr.h
symbolt
Symbol table entry.
Definition: symbol.h:27
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2886
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2816
array_name.h