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 "namespace.h"
16 #include "symbol.h"
17 #include "ssa_expr.h"
18 
19 std::string array_name(
20  const namespacet &ns,
21  const exprt &expr)
22 {
23  if(expr.id()==ID_index)
24  {
25  if(expr.operands().size()!=2)
26  throw "index takes two operands";
27 
28  return array_name(ns, expr.op0())+"[]";
29  }
30  else if(is_ssa_expr(expr))
31  {
32  const symbolt &symbol=
33  ns.lookup(to_ssa_expr(expr).get_object_name());
34  return "array `"+id2string(symbol.base_name)+"'";
35  }
36  else if(expr.id()==ID_symbol)
37  {
38  const symbolt &symbol=ns.lookup(expr);
39  return "array `"+id2string(symbol.base_name)+"'";
40  }
41  else if(expr.id()==ID_string_constant)
42  {
43  return "string constant";
44  }
45  else if(expr.id()==ID_member)
46  {
47  assert(expr.operands().size()==1);
48  return array_name(ns, expr.op0())+"."+
49  expr.get_string(ID_component_name);
50  }
51 
52  return "array";
53 }
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
exprt & op0()
Definition: expr.h:84
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const irep_idt & id() const
Definition: irep.h:189
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Base class for all expressions.
Definition: expr.h:46
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:169
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
Misc Utilities.
operandst & operands()
Definition: expr.h:70
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19