cprover
|
#include <c_typecheck_base.h>
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 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 314 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.
Create symbols for parameter of the code-typed symbol symbol
.
Definition at line 986 of file c_typecheck_base.cpp.
Definition at line 62 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1318 of file c_typecheck_expr.cpp.
Definition at line 1693 of file c_typecheck_type.cpp.
Definition at line 645 of file c_typecheck_base.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 4652 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.
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 2500 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 3931 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 13 of file c_typecheck_typecast.cpp.
Definition at line 68 of file c_typecheck_typecast.cpp.
|
protectedvirtual |
Definition at line 42 of file c_typecheck_typecast.cpp.
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.
Definition at line 366 of file c_typecheck_code.cpp.
Definition at line 299 of file c_typecheck_base.h.
Definition at line 4618 of file c_typecheck_expr.cpp.
Definition at line 4638 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 771 of file c_typecheck_initializer.cpp.
Definition at line 1255 of file c_typecheck_expr.cpp.
Definition at line 282 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.
Definition at line 868 of file c_typecheck_code.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 28 of file c_typecheck_base.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 33 of file c_typecheck_base.cpp.
Implements typecheckt.
Implemented in ansi_c_typecheckt, and cpp_typecheckt.
Definition at line 4160 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 532 of file c_typecheck_type.cpp.
Definition at line 155 of file c_typecheck_code.cpp.
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.
Definition at line 224 of file c_typecheck_code.cpp.
|
protected |
Definition at line 3711 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.
Definition at line 1233 of file c_typecheck_type.cpp.
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.
Definition at line 234 of file c_typecheck_code.cpp.
Definition at line 332 of file c_typecheck_type.cpp.
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.
Reimplemented in cpp_typecheckt.
Definition at line 47 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1716 of file c_typecheck_expr.cpp.
Definition at line 1044 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 3960 of file c_typecheck_expr.cpp.
Definition at line 4290 of file c_typecheck_expr.cpp.
Definition at line 574 of file c_typecheck_expr.cpp.
Definition at line 519 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 510 of file c_typecheck_expr.cpp.
Definition at line 3884 of file c_typecheck_expr.cpp.
Definition at line 557 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1776 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1821 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1260 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 176 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1497 of file c_typecheck_expr.cpp.
Definition at line 734 of file c_typecheck_expr.cpp.
Definition at line 4200 of file c_typecheck_expr.cpp.
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 4089 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1832 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 944 of file c_typecheck_expr.cpp.
Definition at line 809 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1576 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1066 of file c_typecheck_expr.cpp.
Definition at line 3889 of file c_typecheck_expr.cpp.
Definition at line 3919 of file c_typecheck_expr.cpp.
Definition at line 398 of file c_typecheck_code.cpp.
Definition at line 412 of file c_typecheck_code.cpp.
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 3806 of file c_typecheck_expr.cpp.
Definition at line 596 of file c_typecheck_code.cpp.
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.
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 3774 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 4304 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 2042 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.
Definition at line 1000 of file c_typecheck_code.cpp.
Definition at line 884 of file c_typecheck_code.cpp.
Definition at line 1110 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 992 of file c_typecheck_code.cpp.
Definition at line 1048 of file c_typecheck_code.cpp.
Definition at line 1093 of file c_typecheck_code.cpp.
Definition at line 664 of file c_typecheck_code.cpp.
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.
Definition at line 52 of file c_typecheck_base.cpp.
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.
Definition at line 1644 of file c_typecheck_type.cpp.
Definition at line 1608 of file c_typecheck_type.cpp.
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 315 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 278 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.
Definition at line 73 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.