|
CBMC
|
#include <c_typecheck_base.h>
Inheritance diagram for c_typecheck_baset:
Collaboration diagram for c_typecheck_baset: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 |
Protected Attributes inherited from namespacet | |
| const symbol_table_baset * | symbol_table1 |
| const symbol_table_baset * | symbol_table2 |
Additional Inherited Members |
Definition at line 30 of file c_typecheck_base.h.
|
protected |
Definition at line 319 of file c_typecheck_base.h.
|
protected |
Definition at line 78 of file c_typecheck_base.h.
|
inline |
Definition at line 35 of file c_typecheck_base.h.
|
inline |
Definition at line 50 of file c_typecheck_base.h.
|
inlinevirtual |
Definition at line 66 of file c_typecheck_base.h.
Create symbols for parameter of the code-typed symbol symbol.
Definition at line 1001 of file c_typecheck_base.cpp.
Definition at line 61 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1401 of file c_typecheck_expr.cpp.
Definition at line 1704 of file c_typecheck_type.cpp.
Definition at line 657 of file c_typecheck_base.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 2139 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Checks that no history expr or return_value exists in expr.
Definition at line 727 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 754 of file c_typecheck_base.cpp.
|
protected |
Definition at line 250 of file c_typecheck_initializer.cpp.
|
protected |
Definition at line 4863 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.
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 2639 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 1164 of file c_typecheck_type.cpp.
|
protected |
Definition at line 1196 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 96 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 4131 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 123 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.
Definition at line 369 of file c_typecheck_code.cpp.
Definition at line 304 of file c_typecheck_base.h.
Definition at line 4824 of file c_typecheck_expr.cpp.
Definition at line 4847 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 756 of file c_typecheck_initializer.cpp.
Definition at line 1338 of file c_typecheck_expr.cpp.
Definition at line 287 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 869 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 4360 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 576 of file c_typecheck_type.cpp.
Definition at line 158 of file c_typecheck_code.cpp.
Definition at line 192 of file c_typecheck_code.cpp.
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.
Definition at line 227 of file c_typecheck_code.cpp.
|
protected |
Definition at line 3903 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1540 of file c_typecheck_type.cpp.
|
protectedvirtual |
Definition at line 1482 of file c_typecheck_type.cpp.
Definition at line 1254 of file c_typecheck_type.cpp.
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 932 of file c_typecheck_code.cpp.
Definition at line 237 of file c_typecheck_code.cpp.
Definition at line 329 of file c_typecheck_type.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 247 of file c_typecheck_code.cpp.
|
protected |
Definition at line 775 of file c_typecheck_base.cpp.
|
protectedvirtual |
Definition at line 823 of file c_typecheck_code.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 46 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1810 of file c_typecheck_expr.cpp.
Definition at line 1127 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 4160 of file c_typecheck_expr.cpp.
Definition at line 4490 of file c_typecheck_expr.cpp.
Definition at line 626 of file c_typecheck_expr.cpp.
Definition at line 555 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 546 of file c_typecheck_expr.cpp.
Definition at line 4084 of file c_typecheck_expr.cpp.
Definition at line 609 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1870 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1915 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1343 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 175 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1578 of file c_typecheck_expr.cpp.
Definition at line 785 of file c_typecheck_expr.cpp.
Definition at line 4400 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1544 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1413 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1513 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 4289 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1926 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 995 of file c_typecheck_expr.cpp.
Definition at line 860 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1658 of file c_typecheck_expr.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 1149 of file c_typecheck_expr.cpp.
Definition at line 4089 of file c_typecheck_expr.cpp.
Definition at line 4119 of file c_typecheck_expr.cpp.
Definition at line 405 of file c_typecheck_code.cpp.
Definition at line 419 of file c_typecheck_code.cpp.
Definition at line 610 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 4006 of file c_typecheck_expr.cpp.
Definition at line 605 of file c_typecheck_code.cpp.
Definition at line 593 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 494 of file c_typecheck_gcc_polymorphic_builtins.cpp.
|
protectedvirtual |
Definition at line 573 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 599 of file c_typecheck_code.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 628 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 523 of file c_typecheck_code.cpp.
Definition at line 159 of file c_typecheck_base.cpp.
|
protectedvirtual |
Checks an obeys_contract predicate occurrence.
Definition at line 2073 of file c_typecheck_expr.cpp.
|
protected |
Definition at line 319 of file c_typecheck_base.cpp.
|
protected |
Definition at line 189 of file c_typecheck_base.cpp.
|
protectedvirtual |
Definition at line 677 of file c_typecheck_code.cpp.
|
protected |
Definition at line 3966 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 4504 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 2148 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 1782 of file c_typecheck_expr.cpp.
|
protectedvirtual |
Definition at line 962 of file c_typecheck_expr.cpp.
|
virtual |
Definition at line 985 of file c_typecheck_code.cpp.
Definition at line 1001 of file c_typecheck_code.cpp.
Definition at line 885 of file c_typecheck_code.cpp.
Definition at line 1111 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 993 of file c_typecheck_code.cpp.
Definition at line 1049 of file c_typecheck_code.cpp.
Definition at line 1094 of file c_typecheck_code.cpp.
Definition at line 665 of file c_typecheck_code.cpp.
Reimplemented in cpp_typecheckt.
Definition at line 714 of file c_typecheck_code.cpp.
|
protectedvirtual |
Definition at line 536 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 2018 of file c_typecheck_expr.cpp.
Definition at line 1649 of file c_typecheck_type.cpp.
Definition at line 1613 of file c_typecheck_type.cpp.
Definition at line 703 of file c_typecheck_type.cpp.
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 777 of file c_typecheck_code.cpp.
|
protected |
Definition at line 320 of file c_typecheck_base.h.
|
protected |
Definition at line 178 of file c_typecheck_base.h.
|
protected |
Definition at line 180 of file c_typecheck_base.h.
|
protected |
Definition at line 283 of file c_typecheck_base.h.
|
protected |
Definition at line 179 of file c_typecheck_base.h.
|
protected |
Definition at line 76 of file c_typecheck_base.h.
|
protected |
Definition at line 185 of file c_typecheck_base.h.
|
protected |
Definition at line 185 of file c_typecheck_base.h.
Definition at line 75 of file c_typecheck_base.h.
|
protected |
Definition at line 79 of file c_typecheck_base.h.
|
protected |
Definition at line 182 of file c_typecheck_base.h.
|
protected |
Definition at line 181 of file c_typecheck_base.h.
|
protected |
Definition at line 73 of file c_typecheck_base.h.