Skip to content

introduce java_class_typet::componentt #4493

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 8, 2019
Merged

introduce java_class_typet::componentt #4493

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0bf28f0
introduce java_class_typet::componentt
Apr 6, 2019
809c5a3
move is_final to java component type
Apr 6, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ void java_bytecode_convert_classt::convert(
{
class_type.add_base(base);
}
class_typet::componentt base_class_field;
java_class_typet::componentt base_class_field;
base_class_field.type() = class_type.bases().at(0).type();
base_class_field.set_name("@" + id2string(c.super_class));
base_class_field.set_base_name("@" + id2string(c.super_class));
Expand Down Expand Up @@ -798,18 +798,18 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
class_type.set_name(struct_tag_type_identifier);

class_type.components().reserve(3);
class_typet::componentt base_class_component(
java_class_typet::componentt base_class_component(
"@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
base_class_component.set_pretty_name("@java.lang.Object");
base_class_component.set_base_name("@java.lang.Object");
class_type.components().push_back(base_class_component);

class_typet::componentt length_component("length", java_int_type());
java_class_typet::componentt length_component("length", java_int_type());
length_component.set_pretty_name("length");
length_component.set_base_name("length");
class_type.components().push_back(length_component);

class_typet::componentt data_component(
java_class_typet::componentt data_component(
"data", java_reference_type(java_type_from_char(l)));
data_component.set_pretty_name("data");
data_component.set_base_name("data");
Expand Down
37 changes: 36 additions & 1 deletion jbmc/src/java_bytecode/java_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,42 @@ inline bool can_cast_type<annotated_typet>(const typet &)

class java_class_typet:public class_typet
{
public:
public:
class componentt : public class_typet::componentt
{
public:
componentt() = default;

componentt(const irep_idt &_name, typet _type)
: class_typet::componentt(_name, std::move(_type))
{
}

/// is a method 'native'?
bool get_is_native() const
{
return get_bool(ID_is_native_method);
}

/// marks a method as 'native'
void set_is_native(const bool is_native)
{
set(ID_is_native_method, is_native);
}
};

using componentst = std::vector<componentt>;

const componentst &components() const
{
return (const componentst &)(find(ID_components).get_sub());
}

componentst &components()
{
return (componentst &)(add(ID_components).get_sub());
}

const irep_idt &get_access() const
{
return get(ID_access);
Expand Down