CBMC
cpp_scopes.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_scopes.h"
13 
14 #include <util/symbol.h>
15 
16 #include <ostream>
17 
19 {
20  unsigned prefix=++current_scope().compound_counter;
22 }
23 
25  const symbolt &symbol,
26  cpp_scopet &scope,
27  bool is_friend)
28 {
29  PRECONDITION(!symbol.name.empty());
30  PRECONDITION(!symbol.base_name.empty());
31 
32  // functions are also scopes
33  if(symbol.type.id()==ID_code)
34  {
35  cpp_scopest::id_mapt::iterator id_it = id_map.find(symbol.name);
36  if(id_it == id_map.end())
37  {
38  irep_idt block_base_name(std::string("$block:")+symbol.base_name.c_str());
39  cpp_idt &id = scope.insert(block_base_name);
41  id.identifier=symbol.name;
42  id.is_scope=true;
43  id.prefix = id2string(scope.prefix) + id2string(symbol.base_name) + "::";
44  id_map[symbol.name]=&id;
45  }
46  }
47 
48  // should go away, and be replaced by the 'tag only declaration' rule
49  if(is_friend)
50  {
51  cpp_save_scopet saved_scope(*this);
52  go_to(scope);
53 
54  cpp_idt &id=current_scope().insert(symbol.base_name);
55  id.identifier=symbol.name;
56  id.id_class = cpp_idt::id_classt::SYMBOL;
57  if(id_map.find(symbol.name)==id_map.end())
58  id_map[symbol.name]=&id;
59  return id;
60  }
61  else
62  {
63  cpp_idt &id=scope.insert(symbol.base_name);
64  id.identifier=symbol.name;
65  id.id_class = cpp_idt::id_classt::SYMBOL;
66  if(id_map.find(symbol.name)==id_map.end())
67  id_map[symbol.name]=&id;
68  return id;
69  }
70 }
71 
72 void cpp_scopest::print_current(std::ostream &out) const
73 {
74  const cpp_scopet *scope=current_scope_ptr;
75 
76  do
77  {
78  scope->print_fields(out);
79  out << '\n';
80  scope=&scope->get_parent();
81  }
82  while(!scope->is_root_scope());
83 }
Definition: cpp_id.h:23
irep_idt identifier
Definition: cpp_id.h:72
std::string prefix
Definition: cpp_id.h:79
id_classt id_class
Definition: cpp_id.h:45
void print_fields(std::ostream &out, unsigned indent=0) const
Definition: cpp_id.cpp:44
unsigned compound_counter
Definition: cpp_id.h:80
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
void print_current(std::ostream &out) const
Definition: cpp_scopes.cpp:72
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:18
cpp_scopet * current_scope_ptr
Definition: cpp_scopes.h:70
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_scopet & new_scope(const irep_idt &new_scope_name, cpp_idt::id_classt id_class)
Definition: cpp_scopes.h:37
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
id_mapt id_map
Definition: cpp_scopes.h:68
cpp_scopet & get_parent() const
Definition: cpp_scope.h:88
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
bool is_root_scope() const
Definition: cpp_scope.h:77
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
const char * c_str() const
Definition: dstring.h:116
const irep_idt & id() const
Definition: irep.h:388
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Symbol table entry.