cprover
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 "invariant.h"
16 #include "namespace.h"
17 #include "ssa_expr.h"
18 #include "symbol.h"
19 
20 std::string array_name(
21  const namespacet &ns,
22  const exprt &expr)
23 {
24  if(expr.id()==ID_index)
25  {
26  return array_name(ns, to_index_expr(expr).array()) + "[]";
27  }
28  else if(is_ssa_expr(expr))
29  {
30  const symbolt &symbol=
31  ns.lookup(to_ssa_expr(expr).get_object_name());
32  return "array `"+id2string(symbol.base_name)+"'";
33  }
34  else if(expr.id()==ID_symbol)
35  {
36  const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
37  return "array `"+id2string(symbol.base_name)+"'";
38  }
39  else if(expr.id()==ID_string_constant)
40  {
41  return "string constant";
42  }
43  else if(expr.id()==ID_member)
44  {
45  const member_exprt &member_expr = to_member_expr(expr);
46 
47  return array_name(ns, member_expr.compound()) + "." +
48  id2string(member_expr.get_component_name());
49  }
50 
51  return "array";
52 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
Symbol table entry.
Definition: symbol.h:27
Extract member of struct or union.
Definition: std_expr.h:3890
const exprt & compound() const
Definition: std_expr.h:3942
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
Base class for all expressions.
Definition: expr.h:54
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt get_component_name() const
Definition: std_expr.h:3915
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:179
Misc Utilities.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:20