Go to the documentation of this file.
41 if(expr.
id()==ID_symbol)
48 error() <<
"unexpected symbol: " <<
id <<
eom;
68 error() <<
"make_type_compatible got empty type: " << expr.
pretty() <<
eom;
84 error() <<
"failed to typecheck expr "
85 << expr.
pretty() <<
" with type "
87 <<
"; required type " << type.
pretty() <<
eom;
101 if(type.
id()==ID_code)
112 p.set_identifier(
add_prefix(p.get_identifier()));
113 new_symbol.
name=p.get_identifier();
122 new_symbol.
mode=
"jsil";
129 error() <<
"failed to add parameter symbol '" << new_symbol.
name
130 <<
"' in the symbol table" <<
eom;
154 if(expr.
id()==ID_code)
157 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
160 else if(expr.
id()==ID_symbol)
162 else if(expr.
id()==ID_constant)
170 if(expr.
id()==ID_null ||
171 expr.
id()==
"undefined" ||
174 else if(expr.
id()==
"null_type" ||
175 expr.
id()==
"undefined_type" ||
176 expr.
id()==ID_boolean ||
177 expr.
id()==ID_string ||
178 expr.
id()==
"number" ||
179 expr.
id()==
"builtin_object" ||
180 expr.
id()==
"user_object" ||
181 expr.
id()==
"object" ||
182 expr.
id()==ID_pointer ||
183 expr.
id()==ID_member ||
184 expr.
id()==
"variable")
186 else if(expr.
id()==
"proto" ||
188 expr.
id()==
"scope" ||
189 expr.
id()==
"constructid" ||
190 expr.
id()==
"primvalue" ||
191 expr.
id()==
"targetfunction" ||
197 else if(expr.
id()==ID_not)
199 else if(expr.
id()==
"string_to_num")
201 else if(expr.
id()==ID_unary_minus ||
202 expr.
id()==
"num_to_int32" ||
203 expr.
id()==
"num_to_uint32" ||
204 expr.
id()==ID_bitnot)
209 else if(expr.
id()==
"num_to_string")
214 else if(expr.
id()==ID_equal)
216 else if(expr.
id()==ID_lt ||
219 else if(expr.
id()==ID_plus ||
220 expr.
id()==ID_minus ||
221 expr.
id()==ID_mult ||
224 expr.
id()==ID_bitand ||
225 expr.
id()==ID_bitor ||
226 expr.
id()==ID_bitxor ||
231 else if(expr.
id()==ID_and ||
234 else if(expr.
id()==
"subtype_of")
236 else if(expr.
id()==ID_concatenation)
238 else if(expr.
id()==
"ref")
240 else if(expr.
id()==
"field")
242 else if(expr.
id()==ID_base)
244 else if(expr.
id()==ID_typeof)
246 else if(expr.
id()==
"new")
248 else if(expr.
id()==
"hasField")
250 else if(expr.
id()==ID_index)
252 else if(expr.
id()==
"delete")
254 else if(expr.
id()==
"protoField")
256 else if(expr.
id()==
"protoObj")
258 else if(expr.
id()==ID_side_effect)
272 irept &excep_list=expr.
add(ID_exception_list);
273 assert(excep_list.
id()==ID_symbol);
280 if(expr.
id()==ID_null)
282 else if(expr.
id()==
"undefined")
284 else if(expr.
id()==ID_empty)
293 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
308 error() <<
"operator '" << expr.
id() <<
"' expects two operands";
323 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
338 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
359 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
374 error() <<
"operator '" << expr.
id() <<
"' expects single operand" <<
eom;
388 error() <<
"operator '" << expr.
id() <<
"' expects single operand" <<
eom;
402 error() <<
"operator '" << expr.
id() <<
"' expects three operands" <<
eom;
412 if(operand3.
id()==ID_member)
414 else if(operand3.
id()==
"variable")
419 error() <<
"operator '" << expr.
id()
420 <<
"' expects reference type in the third parameter. Got:"
431 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
446 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
461 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
476 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
491 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
505 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
520 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
534 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
548 error() <<
"operator '" << expr.
id() <<
"' expects one operand" <<
eom;
564 identifier==
"eval" ||
567 symbol_tablet::symbolst::const_iterator s_it=
572 error() <<
"unexpected internal symbol: " << identifier <<
eom;
578 const symbolt &symbol=s_it->second;
588 irep_idt identifier_base = identifier;
595 symbol_tablet::symbolst::const_iterator s_it=
602 new_symbol.
name=identifier;
605 new_symbol.
mode=
"jsil";
614 error() <<
"failed to add symbol '" << new_symbol.
name
615 <<
"' in the symbol table" <<
eom;
622 assert(!s_it->second.is_type);
624 const symbolt &symbol=s_it->second;
636 if(statement==ID_function_call)
638 else if(statement==ID_return)
640 else if(statement==ID_expression)
645 error() <<
"expression statement expected to have one operand"
652 else if(statement==ID_label)
657 else if(statement==ID_block)
659 else if(statement==ID_ifthenelse)
661 else if(statement==ID_goto)
665 else if(statement==ID_assign)
667 else if(statement==ID_try_catch)
669 else if(statement==ID_skip)
675 error() <<
"unexpected statement: " << statement <<
eom;
698 error() <<
"try_catch expected to have three operands" <<
eom;
716 error() <<
"function call expected to have three operands" <<
eom;
730 if(f.
id()==ID_symbol)
736 const symbolt &s=*maybe_symbol;
742 for(std::size_t i=0; i<
codet.parameters().size(); i++)
759 for(std::size_t i=call.
arguments().size();
789 new_symbol.
mode=
"jsil";
798 error() <<
"failed to add expression symbol to symbol table"
842 if(symbol.
value.
id()!=
"no-body-just-yet")
850 else if(symbol.
name==
"eval")
854 else if(symbol.
value.
id()==
"no-body-just-yet")
861 error() <<
"non-type symbol value expected code, but got "
872 std::vector<irep_idt> identifiers;
876 identifiers.push_back(symbol_pair.first);
881 for(
const irep_idt &
id : identifiers)
889 for(
const irep_idt &
id : identifiers)
910 const unsigned errors_before=
934 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)
std::size_t size() const
Amount of nodes this expression tree contains.
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.
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
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.
bool has_prefix(const std::string &s, const std::string &prefix)
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.
API to expression classes.
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.