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 }
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19
Misc Utilities.
Base class for all expressions.
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:384
Extract member of struct or union.
Definition: std_expr.h:2841
const exprt & compound() const
Definition: std_expr.h:2890
irep_idt get_component_name() const
Definition: std_expr.h:2863
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
Symbol table entry.