Go to the documentation of this file.
42 if(expr.
id()==ID_symbol)
49 error() <<
"unexpected symbol: " <<
id <<
eom;
69 error() <<
"make_type_compatible got empty type: " << expr.
pretty() <<
eom;
85 error() <<
"failed to typecheck expr "
86 << expr.
pretty() <<
" with type "
88 <<
"; required type " << type.
pretty() <<
eom;
102 if(type.
id()==ID_code)
113 p.set_identifier(
add_prefix(p.get_identifier()));
114 new_symbol.
name=p.get_identifier();
123 new_symbol.
mode=
"jsil";
130 error() <<
"failed to add parameter symbol '" << new_symbol.
name
131 <<
"' in the symbol table" <<
eom;
155 if(expr.
id()==ID_code)
158 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
161 else if(expr.
id()==ID_symbol)
163 else if(expr.
id()==ID_constant)
171 if(expr.
id()==ID_null ||
172 expr.
id()==
"undefined" ||
175 else if(expr.
id()==
"null_type" ||
176 expr.
id()==
"undefined_type" ||
177 expr.
id()==ID_boolean ||
178 expr.
id()==ID_string ||
179 expr.
id()==
"number" ||
180 expr.
id()==
"builtin_object" ||
181 expr.
id()==
"user_object" ||
182 expr.
id()==
"object" ||
183 expr.
id()==ID_pointer ||
184 expr.
id()==ID_member ||
185 expr.
id()==
"variable")
187 else if(expr.
id()==
"proto" ||
189 expr.
id()==
"scope" ||
190 expr.
id()==
"constructid" ||
191 expr.
id()==
"primvalue" ||
192 expr.
id()==
"targetfunction" ||
198 else if(expr.
id()==ID_not)
200 else if(expr.
id()==
"string_to_num")
202 else if(expr.
id()==ID_unary_minus ||
203 expr.
id()==
"num_to_int32" ||
204 expr.
id()==
"num_to_uint32" ||
205 expr.
id()==ID_bitnot)
210 else if(expr.
id()==
"num_to_string")
215 else if(expr.
id()==ID_equal)
217 else if(expr.
id()==ID_lt ||
220 else if(expr.
id()==ID_plus ||
221 expr.
id()==ID_minus ||
222 expr.
id()==ID_mult ||
225 expr.
id()==ID_bitand ||
226 expr.
id()==ID_bitor ||
227 expr.
id()==ID_bitxor ||
232 else if(expr.
id()==ID_and ||
235 else if(expr.
id()==
"subtype_of")
237 else if(expr.
id()==ID_concatenation)
239 else if(expr.
id()==
"ref")
241 else if(expr.
id()==
"field")
243 else if(expr.
id()==ID_base)
245 else if(expr.
id()==ID_typeof)
247 else if(expr.
id()==
"new")
249 else if(expr.
id()==
"hasField")
251 else if(expr.
id()==ID_index)
253 else if(expr.
id()==
"delete")
255 else if(expr.
id()==
"protoField")
257 else if(expr.
id()==
"protoObj")
259 else if(expr.
id()==ID_side_effect)
273 irept &excep_list=expr.
add(ID_exception_list);
274 assert(excep_list.
id()==ID_symbol);
281 if(expr.
id()==ID_null)
283 else if(expr.
id()==
"undefined")
285 else if(expr.
id()==ID_empty)
294 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
309 error() <<
"operator '" << expr.
id() <<
"' expects two operands";
324 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
339 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
360 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
375 error() <<
"operator '" << expr.
id() <<
"' expects single operand" <<
eom;
389 error() <<
"operator '" << expr.
id() <<
"' expects single operand" <<
eom;
403 error() <<
"operator '" << expr.
id() <<
"' expects three operands" <<
eom;
413 if(operand3.
id()==ID_member)
415 else if(operand3.
id()==
"variable")
420 error() <<
"operator '" << expr.
id()
421 <<
"' expects reference type in the third parameter. Got:"
432 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
447 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
462 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
477 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
492 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
506 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
521 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
535 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
549 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
565 identifier==
"eval" ||
568 symbol_tablet::symbolst::const_iterator s_it=
573 error() <<
"unexpected internal symbol: " << identifier <<
eom;
579 const symbolt &symbol=s_it->second;
589 irep_idt identifier_base = identifier;
596 symbol_tablet::symbolst::const_iterator s_it=
603 new_symbol.
name=identifier;
606 new_symbol.
mode=
"jsil";
615 error() <<
"failed to add symbol '" << new_symbol.
name
616 <<
"' in the symbol table" <<
eom;
623 assert(!s_it->second.is_type);
625 const symbolt &symbol=s_it->second;
637 if(statement==ID_function_call)
639 else if(statement==ID_return)
641 else if(statement==ID_expression)
646 error() <<
"expression statement expected to have one operand"
653 else if(statement==ID_label)
658 else if(statement==ID_block)
660 else if(statement==ID_ifthenelse)
662 else if(statement==ID_goto)
666 else if(statement==ID_assign)
668 else if(statement==ID_try_catch)
670 else if(statement==ID_skip)
676 error() <<
"unexpected statement: " << statement <<
eom;
699 error() <<
"try_catch expected to have three operands" <<
eom;
717 error() <<
"function call expected to have three operands" <<
eom;
731 if(f.
id()==ID_symbol)
737 const symbolt &s=*maybe_symbol;
743 for(std::size_t i=0; i<
codet.parameters().size(); i++)
760 for(std::size_t i=call.
arguments().size();
761 i<
codet.parameters().size();
790 new_symbol.
mode=
"jsil";
799 error() <<
"failed to add expression symbol to symbol table"
843 if(symbol.
value.
id()!=
"no-body-just-yet")
851 else if(symbol.
name==
"eval")
855 else if(symbol.
value.
id()==
"no-body-just-yet")
862 error() <<
"non-type symbol value expected code, but got "
873 std::vector<irep_idt> identifiers;
877 identifiers.push_back(symbol_pair.first);
882 for(
const irep_idt &
id : identifiers)
890 for(
const irep_idt &
id : identifiers)
911 const unsigned errors_before=
935 catch(
const std::string &e)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
void typecheck_expr_operands(exprt &expr)
void update_expr_type(exprt &expr, const typet &type)
void typecheck_expr_has_field(exprt &expr)
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
void typecheck_expr_binary_compare(exprt &expr)
#define Forall_operands(it, expr)
void typecheck_expr_unary_string(exprt &expr)
void typecheck_expr_ref(exprt &expr)
void typecheck_function_call(code_function_callt &function_call)
virtual std::string to_string(const exprt &expr)
The type of an expression, extends irept.
const codet & then_case() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_assign(code_assignt &code)
void typecheck_expr_base(exprt &expr)
codet representation of a try/catch block.
typet type
Type of symbol.
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
codet & get_catch_code(unsigned i)
void typecheck_try_catch(code_try_catcht &code)
irept & add(const irep_namet &name)
Fixed-width bit-vector with IEEE floating-point interpretation.
void typecheck_type(typet &type)
void typecheck_expr_index(exprt &expr)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
void typecheck_code(codet &code)
const exprt & cond() const
Expression to hold a symbol (variable)
void typecheck_return(code_returnt &code)
codet representation of an if-then-else statement.
bool jsil_incompatible_types(const typet &type1, const typet &type2)
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
void typecheck_expr_unary_num(exprt &expr)
typet jsil_value_or_reference_type()
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
typet jsil_reference_type()
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
irep_idt mode
Language mode.
bool has_prefix(const std::string &s, const std::string &prefix)
void typecheck_expr_main(exprt &expr)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
std::string type2jsil(const typet &type, const namespacet &ns)
source_locationt source_location
typet jsil_union(const typet &type1, const typet &type2)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const irep_idt & get_identifier() const
Pre-defined bitvector types.
const code_labelt & to_code_label(const codet &code)
typet jsil_variable_reference_type()
void typecheck_expr_unary_boolean(exprt &expr)
void typecheck_expr_proto_field(exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
typet jsil_undefined_type()
void typecheck_ifthenelse(code_ifthenelset &code)
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
const code_returnt & to_code_return(const codet &code)
const parameterst & parameters() const
void typecheck_expr_proto_obj(exprt &expr)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_binary_boolean(exprt &expr)
const code_try_catcht & to_code_try_catch(const codet &code)
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
symbol_table_baset & symbol_table
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void typecheck_expr_constant(exprt &expr)
bool has_return_value() const
exprt value
Initial value of symbol.
typet jsil_member_reference_type()
codet representation of a "return from a function" statement.
const code_assignt & to_code_assign(const codet &code)
source_locationt location
Source code location of definition of symbol.
bool is_jsil_builtin_code_type(const typet &type)
void typecheck_type_symbol(symbolt &)
void typecheck_expr_concatenation(exprt &expr)
std::string expr2jsil(const exprt &expr, const namespacet &ns)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
void typecheck_block(codet &code)
const codet & else_case() const
bool jsil_is_subtype(const typet &type1, const typet &type2)
bool is_jsil_spec_code_type(const typet &type)
void typecheck_expr_binary_arith(exprt &expr)
typet jsil_user_object_type()
typet jsil_value_or_empty_type()
A side_effect_exprt representation of a side effect that throws an exception.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
void typecheck_expr_subtype(exprt &expr)
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
void typecheck_expr_field(exprt &expr)
const exprt & return_value() const
A codet representing an assignment in the program.
const irep_idt & get_statement() const
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const source_locationt & source_location() const
void set_identifier(const irep_idt &identifier)
irep_idt name
The unique identifier.
void typecheck_exp_binary_equal(exprt &expr)
void make_type_compatible(exprt &expr, const typet &type, bool must)
std::size_t get_message_count(unsigned level) const
void typecheck_expr_delete(exprt &expr)
Data structure for representing an arbitrary statement in a program.