cprover
ansi_c_typecheckt Class Reference

#include <ansi_c_typecheck.h>

Inheritance diagram for ansi_c_typecheckt:
[legend]
Collaboration diagram for ansi_c_typecheckt:
[legend]

Public Member Functions

 ansi_c_typecheckt (ansi_c_parse_treet &_parse_tree, symbol_tablet &_symbol_table, const std::string &_module, message_handlert &_message_handler)
 
 ansi_c_typecheckt (ansi_c_parse_treet &_parse_tree, symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2, const std::string &_module, message_handlert &_message_handler)
 
virtual ~ansi_c_typecheckt ()
 
virtual void typecheck ()
 
- Public Member Functions inherited from c_typecheck_baset
 c_typecheck_baset (symbol_tablet &_symbol_table, const std::string &_module, message_handlert &_message_handler)
 
 c_typecheck_baset (symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2, const std::string &_module, message_handlert &_message_handler)
 
virtual ~c_typecheck_baset ()
 
virtual void typecheck_expr (exprt &expr)
 
- Public Member Functions inherited from typecheckt
 typecheckt (message_handlert &_message_handler)
 
virtual ~typecheckt ()
 
void err_location (const source_locationt &loc)
 
void err_location (const exprt &src)
 
void err_location (const typet &src)
 
virtual bool typecheck_main ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 
- Public Member Functions inherited from namespacet
 namespacet (const symbol_tablet &_symbol_table)
 
 namespacet (const symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2)
 
 namespacet (const symbol_tablet *_symbol_table1, const symbol_tablet *_symbol_table2)
 
bool lookup (const irep_idt &name, const symbolt *&symbol) const override
 See 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_tabletget_symbol_table () const
 
const symboltlookup (const irep_idt &name) const
 
const symboltlookup (const symbol_exprt &) const
 
const symboltlookup (const symbol_typet &) const
 
const symboltlookup (const tag_typet &) const
 
virtual bool lookup (const irep_idt &name, const symbolt *&symbol) const=0
 Searches for a symbol named name. More...
 
- Public Member Functions inherited from namespace_baset
const symboltlookup (const irep_idt &name) const
 
const symboltlookup (const symbol_exprt &) const
 
const symboltlookup (const symbol_typet &) const
 
const symboltlookup (const tag_typet &) const
 
virtual ~namespace_baset ()
 
void follow_macros (exprt &) const
 
const typetfollow (const typet &) const
 
const typetfollow_tag (const union_tag_typet &) const
 
const typetfollow_tag (const struct_tag_typet &) const
 
const typetfollow_tag (const c_enum_tag_typet &) const
 

Protected Attributes

ansi_c_parse_treetparse_tree
 
- Protected Attributes inherited from c_typecheck_baset
symbol_tabletsymbol_table
 
const irep_idt module
 
const irep_idt mode
 
symbolt current_symbol
 
id_type_mapt parameter_map
 
bool break_is_allowed
 
bool continue_is_allowed
 
bool case_is_allowed
 
typet switch_op_type
 
typet return_type
 
std::map< irep_idt, source_locationtlabels_defined
 
std::map< irep_idt, source_locationtlabels_used
 
std::list< codetclean_code
 
asm_label_mapt asm_label_map
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 
- Protected Attributes inherited from namespacet
const symbol_tabletsymbol_table1
 
const symbol_tabletsymbol_table2
 

Additional Inherited Members

- Public Types inherited from messaget
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 Public Member Functions inherited from messaget
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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Protected Types inherited from c_typecheck_baset
typedef std::unordered_map< irep_idt, typetid_type_mapt
 
typedef std::unordered_map< irep_idt, irep_idtasm_label_mapt
 
- Protected Member Functions inherited from c_typecheck_baset
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 (codet &code)
 
virtual void typecheck_block (codet &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 (codet &code)
 
virtual void typecheck_gcc_local_label (codet &code)
 
virtual void typecheck_return (codet &code)
 
virtual void typecheck_switch (code_switcht &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_spec_expr (codet &code, const irep_idt &spec)
 
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 (const 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_relation_exprt &expr)
 
virtual void adjust_float_rel (exprt &expr)
 
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)
 
virtual exprt do_special_functions (side_effect_expr_function_callt &expr)
 
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 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_symbol_type (symbol_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 (vector_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
 
typet enum_underlying_type (const mp_integer &min, const mp_integer &max, bool is_packed) const
 
void make_already_typechecked (typet &dest)
 
void add_argc_argv (const symbolt &main_symbol)
 
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)
 
virtual void do_initializer (symbolt &symbol)
 
void apply_asm_label (const irep_idt &asm_label, symbolt &symbol)
 
- Static Protected Member Functions inherited from c_typecheck_baset
static void add_rounding_mode (exprt &)
 
static bool is_numeric_type (const typet &src)
 

Detailed Description

Definition at line 29 of file ansi_c_typecheck.h.

Constructor & Destructor Documentation

◆ ansi_c_typecheckt() [1/2]

ansi_c_typecheckt::ansi_c_typecheckt ( ansi_c_parse_treet _parse_tree,
symbol_tablet _symbol_table,
const std::string &  _module,
message_handlert _message_handler 
)
inline

Definition at line 32 of file ansi_c_typecheck.h.

◆ ansi_c_typecheckt() [2/2]

ansi_c_typecheckt::ansi_c_typecheckt ( ansi_c_parse_treet _parse_tree,
symbol_tablet _symbol_table1,
const symbol_tablet _symbol_table2,
const std::string &  _module,
message_handlert _message_handler 
)
inline

Definition at line 42 of file ansi_c_typecheck.h.

◆ ~ansi_c_typecheckt()

virtual ansi_c_typecheckt::~ansi_c_typecheckt ( )
inlinevirtual

Definition at line 54 of file ansi_c_typecheck.h.

Member Function Documentation

◆ typecheck()

void ansi_c_typecheckt::typecheck ( )
virtual

Member Data Documentation

◆ parse_tree

ansi_c_parse_treet& ansi_c_typecheckt::parse_tree
protected

Definition at line 59 of file ansi_c_typecheck.h.

Referenced by typecheck().


The documentation for this class was generated from the following files: