Skip to content

Commit 4a514e4

Browse files
author
Daniel Kroening
committed
introduce java_class_typet::methodt
This has three benefits: * Ordinary fields no longer have get_is_native/set_is_native, which isn't applicable. * Java methods now offer final/native getters/setters. * Java methods now have the type java_method_typet.
1 parent 850ce41 commit 4a514e4

File tree

1 file changed

+59
-13
lines changed

1 file changed

+59
-13
lines changed

jbmc/src/java_bytecode/java_types.h

Lines changed: 59 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -208,13 +208,65 @@ class java_class_typet:public class_typet
208208
{
209209
}
210210

211-
/// is a method or field 'final'?
211+
/// is a field 'final'?
212212
bool get_is_final() const
213213
{
214214
return get_bool(ID_final);
215215
}
216216

217-
/// is a method or field 'final'?
217+
/// is a field 'final'?
218+
void set_is_final(const bool is_final)
219+
{
220+
set(ID_final, is_final);
221+
}
222+
};
223+
224+
using componentst = std::vector<componentt>;
225+
226+
const componentst &components() const
227+
{
228+
return (const componentst &)(find(ID_components).get_sub());
229+
}
230+
231+
componentst &components()
232+
{
233+
return (componentst &)(add(ID_components).get_sub());
234+
}
235+
236+
const componentt &get_component(const irep_idt &component_name) const
237+
{
238+
return static_cast<const componentt &>(
239+
class_typet::get_component(component_name));
240+
}
241+
242+
class methodt : public class_typet::methodt
243+
{
244+
public:
245+
methodt() = delete;
246+
247+
methodt(const irep_idt &_name, java_method_typet _type)
248+
: class_typet::methodt(_name, std::move(_type))
249+
{
250+
}
251+
252+
const java_method_typet &type() const
253+
{
254+
return static_cast<const java_method_typet &>(
255+
class_typet::methodt::type());
256+
}
257+
258+
java_method_typet &type()
259+
{
260+
return static_cast<java_method_typet &>(class_typet::methodt::type());
261+
}
262+
263+
/// is a method 'final'?
264+
bool get_is_final() const
265+
{
266+
return get_bool(ID_final);
267+
}
268+
269+
/// is a method 'final'?
218270
void set_is_final(const bool is_final)
219271
{
220272
set(ID_final, is_final);
@@ -233,22 +285,16 @@ class java_class_typet:public class_typet
233285
}
234286
};
235287

236-
using componentst = std::vector<componentt>;
288+
using methodst = std::vector<methodt>;
237289

238-
const componentst &components() const
290+
const methodst &methods() const
239291
{
240-
return (const componentst &)(find(ID_components).get_sub());
292+
return (const methodst &)(find(ID_methods).get_sub());
241293
}
242294

243-
componentst &components()
295+
methodst &methods()
244296
{
245-
return (componentst &)(add(ID_components).get_sub());
246-
}
247-
248-
const componentt &get_component(const irep_idt &component_name) const
249-
{
250-
return static_cast<const componentt &>(
251-
class_typet::get_component(component_name));
297+
return (methodst &)(add(ID_methods).get_sub());
252298
}
253299

254300
using static_membert = componentt;

0 commit comments

Comments
 (0)