28 if(expr.
id()==ID_code)
31 if(expr.
id()==ID_typecast && expr.
type().
id()==ID_pointer)
38 if(expr.
id()==ID_symbol)
40 else if(expr.
id()==ID_side_effect)
43 if(statement==ID_java_new)
45 else if(statement==ID_java_new_array)
48 else if(expr.
id()==ID_java_string_literal)
50 else if(expr.
id()==ID_member)
71 std::ostringstream escaped;
72 for(
auto &ch : toescape)
95 for(
const auto c : in)
103 const symbol_typet string_type(
"java::java.lang.String");
105 std::string escaped_symbol_name=
106 "java::java.lang.String.Literal.";
118 new_symbol.
name=escaped_symbol_name;
119 new_symbol.
type=string_type;
122 new_symbol.
mode=ID_java;
134 jlo_init.copy_to_operands(
136 "java::java.lang.String",
137 jlo_struct.components()[0].type()));
138 jlo_init.copy_to_operands(
141 jlo_struct.components()[1].type()));
152 array_symbol.
name=escaped_symbol_name+
"_constarray";
155 array_symbol.
base_name=
"Literal_constarray";
157 array_symbol.
mode=ID_java;
165 array_symbol.
value=literal_array;
168 throw "failed to add constarray symbol to symbol table";
172 jls_struct.components()[1].type()));
176 new_symbol.
value=literal_init;
178 else if(jls_struct.components().size()>=1 &&
179 jls_struct.components()[0].get_name()==
"@java.lang.Object")
186 for(
const auto &comp : jls_struct.components())
188 if(comp.get_name()==
"@java.lang.Object")
196 new_symbol.
value=literal_init;
198 else if(jls_struct.get_bool(ID_incomplete_class))
202 new_symbol.
value=jlo_init;
207 error() <<
"failed to add string literal symbol to symbol table" <<
eom;
219 symbol_tablet::symbolst::const_iterator s_it=
228 new_symbol.
name=identifier;
232 new_symbol.
mode=ID_java;
235 if(new_symbol.
type.
id()==ID_code)
246 error() <<
"failed to add expression symbol to symbol table" <<
eom;
253 assert(!s_it->second.is_type);
255 const symbolt &symbol=s_it->second;
285 if(struct_type.
get_bool(ID_incomplete_class))
291 auto &add_to_components=
295 add_to_components.back().set_base_name(component_name);
296 add_to_components.back().set_pretty_name(component_name);
300 if(components.empty())
312 warning() <<
"failed to find field `" 313 << component_name <<
"` in class hierarchy" <<
eom;
const irep_idt & get_name() const
The type of an expression.
irep_idt name
The unique identifier.
const typet & follow(const typet &src) const
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
Linking: Zero Initialization.
const std::string & id2string(const irep_idt &d)
static std::string escape_non_alnum(const std::string &toescape)
void typecheck_type(typet &)
irep_idt mode
Language mode.
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
void move_to_operands(exprt &expr)
exprt value
Initial value of symbol.
const componentst & components() const
static array_exprt utf16_to_array(const std::wstring &in)
Convert UCS-2 or UTF-16 to an array expression.
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
JAVA Bytecode Language Type Checking.
const irep_idt & id() const
An expression denoting infinity.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
A reference into the symbol table.
void typecheck_code(codet &)
source_locationt source_location
API to expression classes.
const irep_idt & get(const irep_namet &name) const
A side effect that returns a non-deterministically chosen value.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void typecheck_expr_java_new_array(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
Operator to return the address of an object.
bool has_component(const irep_idt &component_name) const
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
std::wstring utf8_to_utf16_little_endian(const std::string &in)
symbol_tablet & symbol_table
typet type
Type of symbol.
Base class for all expressions.
const exprt & struct_op() const
irep_idt base_name
Base (non-scoped) name.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const source_locationt & source_location() const
irep_idt get_component_name() const
void base_type(typet &type, const namespacet &ns)
#define Forall_operands(it, expr)
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
void typecheck_expr_member(member_exprt &)
An expression containing a side effect.
void typecheck_expr_java_new(side_effect_exprt &)
struct constructor from list of elements
void typecheck_expr_symbol(symbol_exprt &)
array constructor from list of elements
exprt make_clean_pointer_cast(const exprt &rawptr, const typet &target_type, const namespacet &ns)
const irep_idt & get_statement() const
bool string_refinement_enabled
void typecheck_expr_java_string_literal(exprt &)