cprover
java_bytecode_parse_tree.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <ostream>
12 
13 #include <util/symbol_table.h>
14 #include <util/namespace.h>
15 
16 #include <langapi/language_util.h>
17 
18 #include "expr2java.h"
19 
21  classt &other)
22 {
23  other.name.swap(name);
24  other.extends.swap(extends);
25  std::swap(other.is_enum, is_enum);
26  std::swap(other.enum_elements, enum_elements);
27  std::swap(other.is_abstract, is_abstract);
28  other.implements.swap(implements);
29  other.fields.swap(fields);
30  other.methods.swap(methods);
31  other.annotations.swap(annotations);
32 }
33 
34 void java_bytecode_parse_treet::output(std::ostream &out) const
35 {
36  parsed_class.output(out);
37 
38  out << "Class references:\n";
39  for(class_refst::const_iterator it=class_refs.begin();
40  it!=class_refs.end();
41  it++)
42  out << " " << *it << '\n';
43 }
44 
45 void java_bytecode_parse_treet::classt::output(std::ostream &out) const
46 {
47  for(const auto &annotation : annotations)
48  {
49  annotation.output(out);
50  out << '\n';
51  }
52 
53  out << "class " << name;
54  if(!extends.empty())
55  out << " extends " << extends;
56  out << " {" << '\n';
57 
58  for(fieldst::const_iterator
59  it=fields.begin();
60  it!=fields.end();
61  it++)
62  {
63  it->output(out);
64  }
65 
66  out << '\n';
67 
68  for(methodst::const_iterator
69  it=methods.begin();
70  it!=methods.end();
71  it++)
72  {
73  it->output(out);
74  }
75 
76  out << '}' << '\n';
77  out << '\n';
78 }
79 
81 {
82  symbol_tablet symbol_table;
83  namespacet ns(symbol_table);
84 
85  out << '@' << type2java(type, ns);
86 
87  if(!element_value_pairs.empty())
88  {
89  out << '(';
90 
91  bool first=true;
92  for(const auto &element_value_pair : element_value_pairs)
93  {
94  if(first)
95  first=false;
96  else
97  out << ", ";
98  element_value_pair.output(out);
99  }
100 
101  out << ')';
102  }
103 }
104 
106  std::ostream &out) const
107 {
108  symbol_tablet symbol_table;
109  namespacet ns(symbol_table);
110 
111  out << '"' << element_name << '"' << '=';
112  out << expr2java(value, ns);
113 }
114 
115 void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
116 {
117  symbol_tablet symbol_table;
118  namespacet ns(symbol_table);
119 
120  for(const auto &annotation : annotations)
121  {
122  out << " ";
123  annotation.output(out);
124  out << '\n';
125  }
126 
127  out << " ";
128 
129  if(is_public)
130  out << "public ";
131 
132  if(is_protected)
133  out << "protected ";
134 
135  if(is_private)
136  out << "private ";
137 
138  if(is_static)
139  out << "static ";
140 
141  if(is_final)
142  out << "final ";
143 
144  if(is_native)
145  out << "native ";
146 
147  if(is_synchronized)
148  out << "synchronized ";
149 
150  out << name;
151  out << " : " << signature;
152 
153  out << '\n';
154 
155  out << " {" << '\n';
156 
157  for(const auto &i : instructions)
158  {
159  if(!i.source_location.get_line().empty())
160  out << " // " << i.source_location << '\n';
161 
162  out << " " << i.address << ": ";
163  out << i.statement;
164 
165  for(std::vector<exprt>::const_iterator
166  a_it=i.args.begin(); a_it!=i.args.end(); a_it++)
167  {
168  if(a_it!=i.args.begin())
169  out << ',';
170  #if 0
171  out << ' ' << from_expr(*a_it);
172  #else
173  out << ' ' << expr2java(*a_it, ns);
174  #endif
175  }
176 
177  out << '\n';
178  }
179 
180  out << " }" << '\n';
181 
182  out << '\n';
183 
184  out << " Locals:\n";
185  for(const auto &v : local_variable_table)
186  {
187  out << " " << v.index << ": " << v.name << ' '
188  << v.signature << '\n';
189  }
190 
191  out << '\n';
192 }
193 
194 void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const
195 {
196  for(const auto &annotation : annotations)
197  {
198  out << " ";
199  annotation.output(out);
200  out << '\n';
201  }
202 
203  out << " ";
204 
205  if(is_public)
206  out << "public ";
207 
208  if(is_static)
209  out << "static ";
210 
211  out << name;
212  out << " : " << signature << ';';
213 
214  out << '\n';
215 }
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:438
virtual void output(std::ostream &out) const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
The symbol table.
Definition: symbol_table.h:52
void output(std::ostream &out) const
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Symbol table.
void output(std::ostream &out) const
void swap(dstringt &b)
Definition: dstring.h:118
virtual void output(std::ostream &out) const
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:431