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 }
array_name
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:20
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
exprt
Base class for all expressions.
Definition: expr.h:53
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:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:128
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3446
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
ssa_expr.h
symbolt
Symbol table entry.
Definition: symbol.h:28
invariant.h
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
array_name.h
Misc Utilities.