replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

use static_members in Java frontend 

An instance of static fields for Java classes.  The Java-specific extension
enables tracking static fields that are final.
This commit is contained in:
Daniel Kroening 2019-04-21 15:03:03 +01:00
parent 55c89cbfc4
commit 385a27cf24
2 changed files with 43 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View File

@ -677,10 +677,37 @@ void java_bytecode_convert_classt::convert(
else
field_type = *java_type_from_string(f.descriptor);
// determine access
irep_idt access;
if(f.is_private)
access = ID_private;
else if(f.is_protected)
access = ID_protected;
else if(f.is_public)
access = ID_public;
else
access = ID_default;
auto &class_type = to_java_class_type(class_symbol.type);
// is this a static field?
if(f.is_static)
{
// Create the symbol; we won't add to the struct type.
const irep_idt field_identifier =
id2string(class_symbol.name) + "." + id2string(f.name);
class_type.static_members().emplace_back();
auto &component = class_type.static_members().back();
component.set_name(field_identifier);
component.set_base_name(f.name);
component.set_pretty_name(f.name);
component.set_access(access);
component.set_is_final(f.is_final);
component.type() = field_type;
// Create the symbol
symbolt new_symbol;
new_symbol.is_static_lifetime=true;
@ -740,26 +767,15 @@ void java_bytecode_convert_classt::convert(
}
else
{
auto &class_type = to_java_class_type(class_symbol.type);
class_type.components().emplace_back();
auto &component = class_type.components().back();
component.set_name(f.name);
component.set_base_name(f.name);
component.set_pretty_name(f.name);
component.type()=field_type;
if(f.is_private)
component.set_access(ID_private);
else if(f.is_protected)
component.set_access(ID_protected);
else if(f.is_public)
component.set_access(ID_public);
else
component.set_access(ID_default);
component.set_access(access);
component.set_is_final(f.is_final);
component.type() = field_type;
// Load annotations
if(!f.annotations.empty())

13
jbmc/src/java_bytecode/java_types.h
View File

@ -155,6 +155,19 @@ public:
class_typet::get_component(component_name));
}
using static_membert = componentt;
using static_memberst = std::vector<componentt>;
const static_memberst &static_members() const
{
return (const static_memberst &)class_typet::static_members();
}
static_memberst &static_members()
{
return (static_memberst &)class_typet::static_members();
}
const irep_idt &get_access() const
{
return get(ID_access);