CBMC
cpp_declarator.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_declarator.h"
13 
14 #include <ansi-c/merged_type.h>
15 
16 #include <ostream>
17 
18 void cpp_declaratort::output(std::ostream &out) const
19 {
20  out << " name: " << name().pretty() << '\n';
21  out << " type: " << type().pretty() << '\n';
22  out << " value: " << value().pretty() << '\n';
23  out << " init_args: " << init_args().pretty() << '\n';
24  out << " method_qualifier: " << method_qualifier().pretty() << '\n';
25 }
26 
27 typet cpp_declaratort::merge_type(const typet &declaration_type) const
28 {
29  typet dest_type=type();
30 
31  if(declaration_type.id()=="cpp-cast-operator")
32  return dest_type;
33 
34  typet *p=&dest_type;
35 
36  // walk down subtype until we hit nil
37  while(true)
38  {
39  typet &t=*p;
40  if(t.is_nil())
41  {
42  t=declaration_type;
43  break;
44  }
45  else if(t.id()==ID_merged_type)
46  {
47  // the chain continues with the last one
48  auto &merged_type = to_merged_type(t);
49  p = &merged_type.last_type();
50  }
51  else
52  {
53  DATA_INVARIANT(!t.id().empty(), "empty type");
54  p = &t.add_subtype();
55  }
56  }
57 
58  return dest_type;
59 }
void output(std::ostream &out) const
irept & method_qualifier()
cpp_namet & name()
typet merge_type(const typet &declaration_type) const
exprt & init_args()
bool empty() const
Definition: dstring.h:89
typet & type()
Return the type of the expression.
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irep_idt & id() const
Definition: irep.h:384
bool is_nil() const
Definition: irep.h:364
The type of an expression, extends irept.
Definition: type.h:29
typet & add_subtype()
Definition: type.h:53
C++ Language Type Checking.
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
Definition: merged_type.h:29
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534