CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
array_name.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Misc Utilities
4
5Author: 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
19std::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 {
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)
Misc Utilities.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2971
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Symbol table entry.
Definition symbol.h:28
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
Symbol table entry.