cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
array_name.h
Misc Utilities.
exprt
Base class for all expressions.
Definition
expr.h:57
irept::id
const irep_idt & id() const
Definition
irep.h:388
member_exprt
Extract member of struct or union.
Definition
std_expr.h:2856
member_exprt::compound
const exprt & compound() const
Definition
std_expr.h:2905
member_exprt::get_component_name
irep_idt get_component_name() const
Definition
std_expr.h:2878
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition
namespace.cpp:134
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition
symbol.h:46
expr.h
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
namespace.h
ssa_expr.h
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
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition
std_expr.h:1484
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition
std_expr.h:2943
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition
std_expr.h:211
symbol.h
Symbol table entry.
util
array_name.cpp
Generated by
1.17.0