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 typet & | follow (const typet &) const |
Resolve type symbol to the type it points to. | |
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. | |
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 316 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 986 of file c_typecheck_base.cpp.
|
staticprotected |
Definition at line 62 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1318 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1693 of file c_typecheck_type.cpp.
Definition at line 645 of file c_typecheck_base.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 2042 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Checks that no history expr or return_value exists in expr.
Definition at line 712 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 739 of file c_typecheck_base.cpp.
|
protected |
Definition at line 257 of file c_typecheck_initializer.cpp.
|
protected |
Definition at line 4659 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 354 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 27 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 231 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 922 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
initialize something of type ‘type’ with given value ‘value’
Definition at line 57 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 2507 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 1143 of file c_typecheck_type.cpp.
|
protected |
Definition at line 1175 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 97 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 3938 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 718 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 1225 of file c_typecheck_gcc_polymorphic_builtins.cpp.
|
protectedvirtual |
Definition at line 366 of file c_typecheck_code.cpp.
|
inlinestaticprotected |
Definition at line 301 of file c_typecheck_base.h.
|
protectedvirtual |
Definition at line 4625 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4645 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 771 of file c_typecheck_initializer.cpp.
|
protectedvirtual |
Definition at line 1255 of file c_typecheck_expr.cpp.
|
inlineprotected |
Definition at line 284 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 868 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 4167 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 532 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 155 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 189 of file c_typecheck_code.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 205 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 224 of file c_typecheck_code.cpp.
|
protected |
Definition at line 3718 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1528 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 1468 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 1233 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 434 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 897 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 762 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 931 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 234 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 332 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 244 of file c_typecheck_code.cpp.
|
protected |
Definition at line 760 of file c_typecheck_base.cpp.
|
protectedvirtual |
Definition at line 822 of file c_typecheck_code.cpp.
|
virtual |
Reimplemented in cpp_typecheckt.
Definition at line 47 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1716 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1044 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 3967 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4297 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 574 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 519 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 510 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 3891 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 557 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1776 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1821 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1260 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 176 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1497 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 734 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4207 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1463 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1330 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1432 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4096 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1832 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 944 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 809 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1576 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1066 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 3896 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 3926 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 398 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 412 of file c_typecheck_code.cpp.
|
protected |
Definition at line 598 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 3813 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 596 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 584 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 493 of file c_typecheck_gcc_polymorphic_builtins.cpp.
|
protectedvirtual |
Definition at line 565 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 590 of file c_typecheck_code.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 619 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 516 of file c_typecheck_code.cpp.
|
protected |
Definition at line 148 of file c_typecheck_base.cpp.
|
protectedvirtual |
Checks an obeys_contract predicate occurrence.
Definition at line 1976 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 308 of file c_typecheck_base.cpp.
|
protected |
Definition at line 178 of file c_typecheck_base.cpp.
|
protectedvirtual |
Definition at line 676 of file c_typecheck_code.cpp.
|
protected |
Definition at line 3781 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 1390 of file c_typecheck_gcc_polymorphic_builtins.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 4311 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 2051 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1688 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 911 of file c_typecheck_expr.cpp.
|
virtual |
Definition at line 984 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 1000 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 884 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 1110 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 992 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 1048 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 1093 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 664 of file c_typecheck_code.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 713 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 529 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 1921 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 666 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 776 of file c_typecheck_code.cpp.
|
protected |
Definition at line 317 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 280 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.