12 #ifndef CPROVER_ANSI_C_C_TYPECHECK_BASE_H 13 #define CPROVER_ANSI_C_C_TYPECHECK_BASE_H 32 const std::string &_module,
45 const std::string &_module,
66 typedef std::unordered_map<irep_idt, typet, irep_id_hash>
id_type_mapt;
95 const exprt &initializer_list,
96 exprt::operandst::const_iterator init_it,
221 bool is_packed)
const;
226 result.subtype().swap(dest);
254 return src.
id()==ID_complex ||
255 src.
id()==ID_unsignedbv ||
256 src.
id()==ID_signedbv ||
257 src.
id()==ID_floatbv ||
258 src.
id()==ID_fixedbv ||
259 src.
id()==ID_c_bool ||
261 src.
id()==ID_c_enum_tag ||
262 src.
id()==ID_c_bit_field;
271 #endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void typecheck_typeof_type(typet &type)
The type of an expression.
std::map< irep_idt, source_locationt > labels_used
std::unordered_map< irep_idt, typet, irep_id_hash > id_type_mapt
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
virtual bool is_complete_type(const typet &type) const
c_typecheck_baset(symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2, const std::string &_module, message_handlert &_message_handler)
virtual void typecheck_start_thread(codet &code)
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
void typecheck_declaration(ansi_c_declarationt &)
A generic base class for relations, i.e., binary predicates.
asm_label_mapt asm_label_map
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_while(code_whilet &code)
c_typecheck_baset(symbol_tablet &_symbol_table, const std::string &_module, message_handlert &_message_handler)
virtual void typecheck_gcc_switch_case_range(codet &code)
virtual void make_constant(exprt &expr)
virtual ~c_typecheck_baset()
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
id_type_mapt parameter_map
The trinary if-then-else operator.
virtual void typecheck_switch_case(code_switch_caset &code)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual void typecheck_symbol_type(typet &type)
virtual std::string to_string(const exprt &expr)
virtual void typecheck_compound_type(struct_union_typet &type)
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual exprt::operandst::const_iterator do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant)
symbol_tablet & symbol_table
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
ANSI-C Language Type Checking.
virtual void typecheck_expr_symbol(exprt &expr)
static bool is_numeric_type(const typet &src)
std::unordered_map< irep_idt, irep_idt, irep_id_hash > asm_label_mapt
const irep_idt & id() const
virtual void typecheck_break(codet &code)
void typecheck_new_symbol(symbolt &symbol)
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
virtual void typecheck_expr_operands(exprt &expr)
virtual void typecheck_c_enum_type(typet &type)
virtual void typecheck_expr_member(exprt &expr)
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_assign(codet &expr)
void make_already_typechecked(typet &dest)
A constant-size array type.
virtual void make_index_type(exprt &expr)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
API to expression classes.
virtual void typecheck_continue(codet &code)
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
void increment_designator(designatort &designator)
void move_symbol(symbolt &symbol)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
A label for branch targets.
virtual void typecheck_expr(exprt &expr)
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual void typecheck_expr_typecast(exprt &expr)
std::list< codet > clean_code
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void typecheck_switch(code_switcht &code)
virtual void typecheck_asm(codet &code)
void designator_enter(const typet &type, designatort &designator)
virtual void typecheck_block(codet &code)
virtual void typecheck_expr_function_identifier(exprt &expr)
typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
virtual void typecheck_custom_type(typet &type)
virtual void adjust_function_parameter(typet &type) const
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
virtual void start_typecheck_code()
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual void typecheck_for(codet &code)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
virtual void typecheck_label(code_labelt &code)
A function call side effect.
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_code_type(code_typet &type)
virtual void typecheck_expr_sizeof(exprt &expr)
virtual void typecheck_vector_type(vector_typet &type)
Base type of C structs and unions, and C++ classes.
virtual void typecheck_gcc_local_label(codet &code)
virtual void typecheck_compound_body(struct_union_typet &type)
Base class for all expressions.
void add_argc_argv(const symbolt &main_symbol)
virtual void typecheck()=0
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_decl(codet &code)
A ‘do while’ instruction.
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void make_constant_index(exprt &expr)
ANSI-CC Language Type Checking.
designatort make_designator(const typet &type, const exprt &src)
std::map< irep_idt, source_locationt > labels_defined
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
void typecheck_symbol(symbolt &symbol)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
virtual void typecheck_array_type(array_typet &type)
virtual void implicit_typecast_arithmetic(exprt &expr)
void typecheck_function_body(symbolt &symbol)
static void add_rounding_mode(exprt &)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A statement in a programming language.
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr_constant(exprt &expr)
virtual void make_constant_rec(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
An expression containing a side effect.
virtual void typecheck_expr_main(exprt &expr)
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_expr_alignof(exprt &expr)
A base class for shift operators.
virtual void typecheck_dowhile(code_dowhilet &code)
virtual void typecheck_return(codet &code)
virtual void typecheck_expr_shifts(shift_exprt &expr)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_code(codet &code)
virtual void typecheck_expression(codet &code)
virtual void adjust_float_rel(exprt &expr)