26 if(expr.
id()==ID_code)
29 if(expr.
id()==ID_typecast &&
30 expr.
type().
id()==ID_pointer)
41 expr.
id() != ID_java_string_literal,
42 "String literals should have been converted to constant globals " 43 "before typecheck_expr");
45 if(expr.
id()==ID_symbol)
47 else if(expr.
id()==ID_side_effect)
50 if(statement==ID_java_new)
52 else if(statement==ID_java_new_array)
55 else if(expr.
id()==ID_member)
79 symbol_tablet::symbolst::const_iterator s_it=
90 new_symbol.
name=identifier;
94 new_symbol.
mode=ID_java;
97 if(new_symbol.
type.
id()==ID_code)
108 error() <<
"failed to add expression symbol to symbol table" <<
eom;
115 INVARIANT(!s_it->second.is_type,
"symbol identifier should not be a type");
117 const symbolt &symbol=s_it->second;
147 if(components.empty())
159 warning() <<
"failed to find field `" 160 << component_name <<
"` in class hierarchy" <<
eom;
const irep_idt & get_name() const
The type of an expression.
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
void typecheck_type(typet &)
irep_idt mode
Language mode.
const irep_idt & get_identifier() const
std::vector< componentt > componentst
const componentst & components() const
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...
static mstreamt & eom(mstreamt &m)
#define INVARIANT(CONDITION, REASON)
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
mstreamt & warning() const
JAVA Bytecode Language Type Checking.
Expression Initialization.
const irep_idt & id() const
symbol_table_baset & symbol_table
void typecheck_code(codet &)
source_locationt source_location
const irep_idt & get(const irep_namet &name) const
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void typecheck_expr_java_new_array(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
bool has_component(const irep_idt &component_name) const
typet type
Type of symbol.
Base class for all expressions.
const exprt & struct_op() const
irep_idt base_name
Base (non-scoped) name.
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)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
void typecheck_expr_member(member_exprt &)
An expression containing a side effect.
void typecheck_expr_java_new(side_effect_exprt &)
void typecheck_expr_symbol(symbol_exprt &)
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
const irep_idt & get_statement() const
Produce code for simple implementation of String Java libraries.