|
| | ansi_c_typecheckt (ansi_c_parse_treet &_parse_tree, symbol_table_baset &_symbol_table, const std::string &_module, message_handlert &_message_handler) |
| |
| | ansi_c_typecheckt (ansi_c_parse_treet &_parse_tree, symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2, const std::string &_module, message_handlert &_message_handler) |
| |
| virtual | ~ansi_c_typecheckt () |
| |
| virtual void | typecheck () |
| |
| | c_typecheck_baset (symbol_table_baset &_symbol_table, const std::string &_module, message_handlert &_message_handler) |
| |
| | c_typecheck_baset (symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2, const std::string &_module, message_handlert &_message_handler) |
| |
| virtual | ~c_typecheck_baset () |
| |
| virtual void | typecheck_expr (exprt &expr) |
| |
| virtual void | typecheck_spec_assigns (exprt::operandst &targets) |
| |
| | typecheckt (message_handlert &_message_handler) |
| |
| virtual | ~typecheckt () |
| |
| virtual bool | typecheck_main () |
| |
| virtual void | set_message_handler (message_handlert &_message_handler) |
| |
| message_handlert & | get_message_handler () |
| |
| | messaget (const messaget &other) |
| |
| messaget & | operator= (const messaget &other) |
| |
| | messaget (message_handlert &_message_handler) |
| |
| virtual | ~messaget () |
| |
| mstreamt & | get_mstream (unsigned message_level) const |
| |
| mstreamt & | error () const |
| |
| mstreamt & | warning () const |
| |
| mstreamt & | result () const |
| |
| mstreamt & | status () const |
| |
| mstreamt & | statistics () const |
| |
| mstreamt & | progress () const |
| |
| mstreamt & | debug () const |
| |
| void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
| | Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
|
| |
| | namespacet (const symbol_table_baset &_symbol_table) |
| |
| | namespacet (const symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2) |
| |
| | namespacet (const symbol_table_baset *_symbol_table1, const symbol_table_baset *_symbol_table2) |
| |
| bool | lookup (const irep_idt &name, const symbolt *&symbol) const override |
| | See documentation for namespace_baset::lookup(). More...
|
| |
| std::size_t | smallest_unused_suffix (const std::string &prefix) const override |
| | See documentation for namespace_baset::smallest_unused_suffix(). More...
|
| |
| const symbol_table_baset & | get_symbol_table () const |
| | Return first symbol table registered with the namespace. More...
|
| |
| const symbolt & | lookup (const irep_idt &name) const |
| | Lookup a symbol in the namespace. More...
|
| |
| const symbolt & | lookup (const symbol_exprt &) const |
| | Generic lookup function for a symbol expression in a symbol table. More...
|
| |
| const symbolt & | lookup (const tag_typet &) const |
| | Generic lookup function for a tag type in a symbol table. More...
|
| |
| virtual bool | lookup (const irep_idt &name, const symbolt *&symbol) const=0 |
| | Searches for a symbol named name. More...
|
| |
| const symbolt & | lookup (const irep_idt &name) const |
| | Lookup a symbol in the namespace. More...
|
| |
| const symbolt & | lookup (const symbol_exprt &) const |
| | Generic lookup function for a symbol expression in a symbol table. More...
|
| |
| const symbolt & | lookup (const tag_typet &) const |
| | Generic lookup function for a tag type in a symbol table. More...
|
| |
| virtual | ~namespace_baset () |
| |
| void | follow_macros (exprt &) const |
| | Follow macros to their values in a given expression. More...
|
| |
| const typet & | follow (const typet &) const |
| | Resolve type symbol to the type it points to. More...
|
| |
| const union_typet & | follow_tag (const union_tag_typet &) const |
| | Follow type tag of union type. More...
|
| |
| const struct_typet & | follow_tag (const struct_tag_typet &) const |
| | Follow type tag of struct type. More...
|
| |
| const c_enum_typet & | follow_tag (const c_enum_tag_typet &) const |
| | Follow type tag of enum type. More...
|
| |
| const struct_union_typet & | follow_tag (const struct_or_union_tag_typet &) const |
| | Resolve a struct_tag_typet or union_tag_typet to the complete version. More...
|
| |
|
| enum | message_levelt {
M_ERROR =1
, M_WARNING =2
, M_RESULT =4
, M_STATUS =6
,
M_STATISTICS =8
, M_PROGRESS =9
, M_DEBUG =10
} |
| |
| static unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
| | Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
|
| |
| static commandt | command (unsigned c) |
| | Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
|
| |
| static eomt | eom |
| |
| static const commandt | reset |
| | return to default formatting, as defined by the terminal More...
|
| |
| static const commandt | red |
| | render text with red foreground color More...
|
| |
| static const commandt | green |
| | render text with green foreground color More...
|
| |
| static const commandt | yellow |
| | render text with yellow foreground color More...
|
| |
| static const commandt | blue |
| | render text with blue foreground color More...
|
| |
| static const commandt | magenta |
| | render text with magenta foreground color More...
|
| |
| static const commandt | cyan |
| | render text with cyan foreground color More...
|
| |
| static const commandt | bright_red |
| | render text with bright red foreground color More...
|
| |
| static const commandt | bright_green |
| | render text with bright green foreground color More...
|
| |
| static const commandt | bright_yellow |
| | render text with bright yellow foreground color More...
|
| |
| static const commandt | bright_blue |
| | render text with bright blue foreground color More...
|
| |
| static const commandt | bright_magenta |
| | render text with bright magenta foreground color More...
|
| |
| static const commandt | bright_cyan |
| | render text with bright cyan foreground color More...
|
| |
| static const commandt | bold |
| | render text with bold font More...
|
| |
| static const commandt | faint |
| | render text with faint font More...
|
| |
| static const commandt | italic |
| | render italic text More...
|
| |
| static const commandt | underline |
| | render underlined text More...
|
| |
| typedef std::unordered_map< irep_idt, typet > | id_type_mapt |
| |
| typedef std::unordered_map< irep_idt, irep_idt > | asm_label_mapt |
| |
| virtual std::string | to_string (const exprt &expr) |
| |
| virtual std::string | to_string (const typet &type) |
| |
| virtual void | do_initializer (exprt &initializer, const typet &type, bool force_constant) |
| |
| virtual exprt | do_initializer_rec (const exprt &value, const typet &type, bool force_constant) |
| | initialize something of type ‘type’ with given value ‘value’ More...
|
| |
| virtual exprt | do_initializer_list (const exprt &value, const typet &type, bool force_constant) |
| |
| 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) |
| |
| designatort | make_designator (const typet &type, const exprt &src) |
| |
| void | designator_enter (const typet &type, designatort &designator) |
| |
| void | increment_designator (designatort &designator) |
| |
| bool | gcc_vector_types_compatible (const vector_typet &, const vector_typet &) |
| |
| virtual void | implicit_typecast (exprt &expr, const typet &type) |
| |
| virtual void | implicit_typecast_arithmetic (exprt &expr) |
| |
| virtual void | implicit_typecast_arithmetic (exprt &expr1, exprt &expr2) |
| |
| virtual void | implicit_typecast_bool (exprt &expr) |
| |
| virtual void | start_typecheck_code () |
| |
| virtual void | typecheck_code (codet &code) |
| |
| virtual void | typecheck_assign (codet &expr) |
| |
| virtual void | typecheck_asm (code_asmt &code) |
| |
| virtual void | typecheck_block (code_blockt &code) |
| |
| virtual void | typecheck_break (codet &code) |
| |
| virtual void | typecheck_continue (codet &code) |
| |
| virtual void | typecheck_decl (codet &code) |
| |
| virtual void | typecheck_expression (codet &code) |
| |
| virtual void | typecheck_for (codet &code) |
| |
| virtual void | typecheck_goto (code_gotot &code) |
| |
| virtual void | typecheck_ifthenelse (code_ifthenelset &code) |
| |
| virtual void | typecheck_label (code_labelt &code) |
| |
| virtual void | typecheck_switch_case (code_switch_caset &code) |
| |
| virtual void | typecheck_gcc_computed_goto (codet &code) |
| |
| virtual void | typecheck_gcc_switch_case_range (code_gcc_switch_case_ranget &) |
| |
| virtual void | typecheck_gcc_local_label (codet &code) |
| |
| virtual void | typecheck_return (code_frontend_returnt &) |
| |
| virtual void | typecheck_switch (codet &code) |
| |
| virtual void | typecheck_while (code_whilet &code) |
| |
| virtual void | typecheck_dowhile (code_dowhilet &code) |
| |
| virtual void | typecheck_start_thread (codet &code) |
| |
| virtual void | typecheck_typed_target_call (side_effect_expr_function_callt &expr) |
| |
| virtual void | typecheck_obeys_contract_call (side_effect_expr_function_callt &expr) |
| | Checks an obeys_contract predicate occurrence. More...
|
| |
| virtual void | check_history_expr_return_value (const exprt &expr, std::string &clause_type) |
| | Checks that no history expr or return_value exists in expr. More...
|
| |
| virtual void | check_was_freed (const exprt &expr, std::string &clause_type) |
| | Checks that no occurence of the CPROVER_PREFIX was_freed predicate is found in expr. More...
|
| |
| virtual void | typecheck_spec_frees (exprt::operandst &targets) |
| |
| virtual void | typecheck_conditional_targets (exprt::operandst &targets, const std::function< void(exprt &)> typecheck_target, const std::string &clause_type) |
| |
| virtual void | typecheck_spec_condition (exprt &condition) |
| |
| virtual void | typecheck_spec_assigns_target (exprt &target) |
| |
| virtual void | typecheck_spec_frees_target (exprt &target) |
| |
| virtual void | typecheck_spec_loop_invariant (codet &code) |
| |
| virtual void | typecheck_spec_decreases (codet &code) |
| |
| virtual void | throw_on_side_effects (const exprt &expr) |
| |
| virtual void | typecheck_expr_builtin_va_arg (exprt &expr) |
| |
| virtual void | typecheck_expr_builtin_offsetof (exprt &expr) |
| |
| virtual void | typecheck_expr_cw_va_arg_typeof (exprt &expr) |
| |
| virtual void | typecheck_expr_main (exprt &expr) |
| |
| virtual void | typecheck_expr_operands (exprt &expr) |
| |
| virtual void | typecheck_expr_comma (exprt &expr) |
| |
| virtual void | typecheck_expr_constant (exprt &expr) |
| |
| virtual void | typecheck_expr_side_effect (side_effect_exprt &expr) |
| |
| virtual void | typecheck_expr_unary_arithmetic (exprt &expr) |
| |
| virtual void | typecheck_expr_unary_boolean (exprt &expr) |
| |
| virtual void | typecheck_expr_binary_arithmetic (exprt &expr) |
| |
| virtual void | typecheck_expr_shifts (shift_exprt &expr) |
| |
| virtual void | typecheck_expr_pointer_arithmetic (exprt &expr) |
| |
| virtual void | typecheck_arithmetic_pointer (exprt &expr) |
| |
| virtual void | typecheck_expr_binary_boolean (exprt &expr) |
| |
| virtual void | typecheck_expr_trinary (if_exprt &expr) |
| |
| virtual void | typecheck_expr_address_of (exprt &expr) |
| |
| virtual void | typecheck_expr_dereference (exprt &expr) |
| |
| virtual void | typecheck_expr_member (exprt &expr) |
| |
| virtual void | typecheck_expr_ptrmember (exprt &expr) |
| |
| virtual void | typecheck_expr_rel (binary_relation_exprt &expr) |
| |
| virtual void | typecheck_expr_rel_vector (binary_exprt &expr) |
| |
| virtual void | adjust_float_rel (binary_relation_exprt &) |
| |
| virtual void | typecheck_expr_index (exprt &expr) |
| |
| virtual void | typecheck_expr_typecast (exprt &expr) |
| |
| virtual void | typecheck_expr_symbol (exprt &expr) |
| |
| virtual void | typecheck_expr_sizeof (exprt &expr) |
| |
| virtual void | typecheck_expr_alignof (exprt &expr) |
| |
| virtual void | typecheck_expr_function_identifier (exprt &expr) |
| |
| virtual void | typecheck_side_effect_gcc_conditional_expression (side_effect_exprt &expr) |
| |
| virtual void | typecheck_side_effect_function_call (side_effect_expr_function_callt &expr) |
| |
| virtual void | typecheck_side_effect_assignment (side_effect_exprt &expr) |
| |
| virtual void | typecheck_side_effect_statement_expression (side_effect_exprt &expr) |
| |
| virtual void | typecheck_function_call_arguments (side_effect_expr_function_callt &expr) |
| | Typecheck the parameters in a function call expression, and where necessary, make implicit casts around parameters explicit. More...
|
| |
| virtual exprt | do_special_functions (side_effect_expr_function_callt &expr) |
| |
| exprt | typecheck_builtin_overflow (side_effect_expr_function_callt &expr, const irep_idt &arith_op) |
| |
| exprt | typecheck_saturating_arithmetic (const side_effect_expr_function_callt &expr) |
| |
| virtual std::optional< symbol_exprt > | typecheck_gcc_polymorphic_builtin (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location) |
| |
| virtual code_blockt | instantiate_gcc_polymorphic_builtin (const irep_idt &identifier, const symbol_exprt &function_symbol) |
| |
| virtual std::optional< symbol_exprt > | typecheck_shadow_memory_builtin (const side_effect_expr_function_callt &expr) |
| | Typecheck the function if it is a shadow_memory builtin and return a symbol for it. More...
|
| |
| virtual exprt | typecheck_shuffle_vector (const side_effect_expr_function_callt &expr) |
| |
| void | disallow_subexpr_by_id (const exprt &, const irep_idt &, const std::string &) const |
| |
| virtual void | make_index_type (exprt &expr) |
| |
| virtual void | make_constant (exprt &expr) |
| |
| virtual void | make_constant_index (exprt &expr) |
| |
| virtual bool | gcc_types_compatible_p (const typet &, const typet &) |
| |
| virtual bool | builtin_factory (const irep_idt &) |
| |
| virtual void | typecheck_type (typet &type) |
| |
| virtual void | typecheck_compound_type (struct_union_typet &type) |
| |
| virtual void | typecheck_compound_body (struct_union_typet &type) |
| |
| virtual void | typecheck_c_enum_type (typet &type) |
| |
| virtual void | typecheck_c_enum_tag_type (c_enum_tag_typet &type) |
| |
| virtual void | typecheck_code_type (code_typet &type) |
| |
| virtual void | typecheck_typedef_type (typet &type) |
| |
| virtual void | typecheck_c_bit_field_type (c_bit_field_typet &type) |
| |
| virtual void | typecheck_typeof_type (typet &type) |
| |
| virtual void | typecheck_array_type (array_typet &type) |
| |
| virtual void | typecheck_vector_type (typet &type) |
| |
| virtual void | typecheck_custom_type (typet &type) |
| |
| virtual void | adjust_function_parameter (typet &type) const |
| |
| virtual bool | is_complete_type (const typet &type) const |
| |
| typet | enum_constant_type (const mp_integer &min, const mp_integer &max) const |
| |
| bitvector_typet | enum_underlying_type (const mp_integer &min, const mp_integer &max, bool is_packed) const |
| |
| void | move_symbol (symbolt &symbol, symbolt *&new_symbol) |
| |
| void | move_symbol (symbolt &symbol) |
| |
| void | typecheck_declaration (ansi_c_declarationt &) |
| |
| void | typecheck_symbol (symbolt &symbol) |
| |
| void | typecheck_new_symbol (symbolt &symbol) |
| |
| void | typecheck_redefinition_type (symbolt &old_symbol, symbolt &new_symbol) |
| |
| void | typecheck_redefinition_non_type (symbolt &old_symbol, symbolt &new_symbol) |
| |
| void | typecheck_function_body (symbolt &symbol) |
| |
| void | add_parameters_to_symbol_table (symbolt &symbol) |
| | Create symbols for parameter of the code-typed symbol symbol. More...
|
| |
| virtual void | do_initializer (symbolt &symbol) |
| |
| void | apply_asm_label (const irep_idt &asm_label, symbolt &symbol) |
| |
| static void | add_rounding_mode (exprt &) |
| |
| static bool | is_numeric_type (const typet &src) |
| |
Inheritance diagram for ansi_c_typecheckt: