cprover
|
#include <c_typecheck_base.h>
Public Member Functions | |
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 ()=0 |
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 () |
![]() | |
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(). | |
std::size_t | smallest_unused_suffix (const std::string &prefix) const override |
See documentation for namespace_baset::smallest_unused_suffix(). | |
const symbol_table_baset & | get_symbol_table () const |
Return first symbol table registered with the namespace. | |
const symbolt & | lookup (const irep_idt &name) const |
Lookup a symbol in the namespace. | |
const symbolt & | lookup (const symbol_exprt &) const |
Generic lookup function for a symbol expression in a symbol table. | |
const symbolt & | lookup (const tag_typet &) const |
Generic lookup function for a tag type in a symbol table. | |
![]() | |
const symbolt & | lookup (const irep_idt &name) const |
Lookup a symbol in the namespace. | |
const symbolt & | lookup (const symbol_exprt &) const |
Generic lookup function for a symbol expression in a symbol table. | |
const symbolt & | lookup (const tag_typet &) const |
Generic lookup function for a tag type in a symbol table. | |
virtual | ~namespace_baset () |
void | follow_macros (exprt &) const |
Follow macros to their values in a given expression. | |
const union_typet & | follow_tag (const union_tag_typet &) const |
Follow type tag of union type. | |
const struct_typet & | follow_tag (const struct_tag_typet &) const |
Follow type tag of struct type. | |
const c_enum_typet & | follow_tag (const c_enum_tag_typet &) const |
Follow type tag of enum type. | |
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. | |
Protected Types | |
typedef std::unordered_map< irep_idt, typet > | id_type_mapt |
typedef std::unordered_map< irep_idt, irep_idt > | asm_label_mapt |
Static Protected Member Functions | |
static void | add_rounding_mode (exprt &) |
static bool | is_numeric_type (const typet &src) |
Protected Attributes | |
symbol_table_baset & | symbol_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_locationt > | labels_defined |
std::map< irep_idt, source_locationt > | labels_used |
std::list< codet > | clean_code |
asm_label_mapt | asm_label_map |
![]() | |
const symbol_table_baset * | symbol_table1 |
const symbol_table_baset * | symbol_table2 |
Additional Inherited Members |
Definition at line 28 of file c_typecheck_base.h.
|
protected |
Definition at line 317 of file c_typecheck_base.h.
|
protected |
Definition at line 76 of file c_typecheck_base.h.
|
inline |
Definition at line 33 of file c_typecheck_base.h.
|
inline |
Definition at line 48 of file c_typecheck_base.h.
|
inlinevirtual |
Definition at line 64 of file c_typecheck_base.h.
|
protected |
Create symbols for parameter of the code-typed symbol symbol
.
Definition at line 996 of file c_typecheck_base.cpp.
|
staticprotected |
Definition at line 61 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1371 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1691 of file c_typecheck_type.cpp.
Definition at line 656 of file c_typecheck_base.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 2111 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Checks that no history expr or return_value exists in expr.
Definition at line 722 of file c_typecheck_base.cpp.
|
protectedvirtual |
Checks that no occurence of the CPROVER_PREFIX was_freed
predicate is found in expr.
Definition at line 749 of file c_typecheck_base.cpp.
|
protected |
Definition at line 250 of file c_typecheck_initializer.cpp.
|
protected |
Definition at line 4780 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 345 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 26 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 224 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 909 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
initialize something of type ‘type’ with given value ‘value’
Definition at line 56 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 2588 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 1159 of file c_typecheck_type.cpp.
|
protected |
Definition at line 1191 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 96 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 4053 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 13 of file c_typecheck_typecast.cpp.
|
protectedvirtual |
Definition at line 68 of file c_typecheck_typecast.cpp.
|
protectedvirtual |
Definition at line 42 of file c_typecheck_typecast.cpp.
|
inlineprotectedvirtual |
Definition at line 121 of file c_typecheck_base.h.
|
protected |
Definition at line 706 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 1238 of file c_typecheck_gcc_polymorphic_builtins.cpp.
|
protectedvirtual |
Definition at line 369 of file c_typecheck_code.cpp.
|
inlinestaticprotected |
Definition at line 302 of file c_typecheck_base.h.
|
protectedvirtual |
Definition at line 4741 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4764 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 756 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 1308 of file c_typecheck_expr.cpp.
|
inlineprotected |
Definition at line 285 of file c_typecheck_base.h.
Definition at line 38 of file c_typecheck_base.cpp.
|
protectedvirtual |
Definition at line 24 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 867 of file c_typecheck_code.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 28 of file c_typecheck_base.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 33 of file c_typecheck_base.cpp.
|
pure virtual |
Implements typecheckt.
Implemented in ansi_c_typecheckt, and cpp_typecheckt.
|
protectedvirtual |
Definition at line 4282 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 576 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 158 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 192 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 424 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 208 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 227 of file c_typecheck_code.cpp.
|
protected |
Definition at line 3825 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1535 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 1477 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 1249 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 29 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 480 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 921 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 789 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 930 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 237 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 329 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 247 of file c_typecheck_code.cpp.
|
protected |
Definition at line 770 of file c_typecheck_base.cpp.
|
protectedvirtual |
Definition at line 821 of file c_typecheck_code.cpp.
|
virtual |
Reimplemented in cpp_typecheckt.
Definition at line 46 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1782 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1097 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 4082 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4412 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 596 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 541 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 532 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4006 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 579 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1842 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1887 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1313 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 175 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1550 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 755 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4322 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1516 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1383 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1485 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4211 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1898 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 965 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 830 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1630 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1119 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4011 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4041 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 405 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 419 of file c_typecheck_code.cpp.
|
protected |
Definition at line 609 of file c_typecheck_base.cpp.
|
protectedvirtual |
Typecheck the parameters in a function call expression, and where necessary, make implicit casts around parameters explicit.
Reimplemented in cpp_typecheckt.
Definition at line 3928 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 603 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 591 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 494 of file c_typecheck_gcc_polymorphic_builtins.cpp.
|
protectedvirtual |
Definition at line 572 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 597 of file c_typecheck_code.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 626 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 523 of file c_typecheck_code.cpp.
|
protected |
Definition at line 158 of file c_typecheck_base.cpp.
|
protectedvirtual |
Checks an obeys_contract predicate occurrence.
Definition at line 2045 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 318 of file c_typecheck_base.cpp.
|
protected |
Definition at line 188 of file c_typecheck_base.cpp.
|
protectedvirtual |
Definition at line 675 of file c_typecheck_code.cpp.
|
protected |
Definition at line 3888 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Typecheck the function if it is a shadow_memory builtin and return a symbol for it.
Otherwise return empty.
Definition at line 226 of file c_typecheck_shadow_memory_builtin.cpp.
|
protectedvirtual |
Definition at line 1403 of file c_typecheck_gcc_polymorphic_builtins.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 4426 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 2120 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1754 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 932 of file c_typecheck_expr.cpp.
|
virtual |
Definition at line 983 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 999 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 883 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 1109 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 991 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 1047 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 1092 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 663 of file c_typecheck_code.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 712 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 536 of file c_typecheck_code.cpp.
|
protected |
Definition at line 52 of file c_typecheck_base.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 34 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 1990 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1644 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 1608 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 703 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 775 of file c_typecheck_code.cpp.
|
protected |
Definition at line 318 of file c_typecheck_base.h.
|
protected |
Definition at line 176 of file c_typecheck_base.h.
|
protected |
Definition at line 178 of file c_typecheck_base.h.
|
protected |
Definition at line 281 of file c_typecheck_base.h.
|
protected |
Definition at line 177 of file c_typecheck_base.h.
|
protected |
Definition at line 74 of file c_typecheck_base.h.
|
protected |
Definition at line 183 of file c_typecheck_base.h.
|
protected |
Definition at line 183 of file c_typecheck_base.h.
|
protected |
Definition at line 73 of file c_typecheck_base.h.
|
protected |
Definition at line 72 of file c_typecheck_base.h.
|
protected |
Definition at line 77 of file c_typecheck_base.h.
|
protected |
Definition at line 180 of file c_typecheck_base.h.
|
protected |
Definition at line 179 of file c_typecheck_base.h.
|
protected |
Definition at line 71 of file c_typecheck_base.h.