cprover
c_typecheck_base.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANSI_C_C_TYPECHECK_BASE_H
13 #define CPROVER_ANSI_C_C_TYPECHECK_BASE_H
14 
15 #include <util/symbol_table.h>
16 #include <util/typecheck.h>
17 #include <util/namespace.h>
18 #include <util/std_code.h>
19 #include <util/std_expr.h>
20 #include <util/std_types.h>
21 
22 #include "ansi_c_declaration.h"
23 #include "designator.h"
24 
26  public typecheckt,
27  public namespacet
28 {
29 public:
31  symbol_tablet &_symbol_table,
32  const std::string &_module,
33  message_handlert &_message_handler):
34  typecheckt(_message_handler),
35  namespacet(_symbol_table),
36  symbol_table(_symbol_table),
37  module(_module),
38  mode(ID_C),
39  break_is_allowed(false),
40  continue_is_allowed(false),
41  case_is_allowed(false)
42  {
43  }
44 
46  symbol_tablet &_symbol_table1,
47  const symbol_tablet &_symbol_table2,
48  const std::string &_module,
49  message_handlert &_message_handler):
50  typecheckt(_message_handler),
51  namespacet(_symbol_table1, _symbol_table2),
52  symbol_table(_symbol_table1),
53  module(_module),
54  mode(ID_C),
55  break_is_allowed(false),
56  continue_is_allowed(false),
57  case_is_allowed(false)
58  {
59  }
60 
61  virtual ~c_typecheck_baset() { }
62 
63  virtual void typecheck()=0;
64  virtual void typecheck_expr(exprt &expr);
65 
66 protected:
69  const irep_idt mode;
71 
72  typedef std::unordered_map<irep_idt, typet> id_type_mapt;
74 
75  // overload to use language specific syntax
76  virtual std::string to_string(const exprt &expr);
77  virtual std::string to_string(const typet &type);
78 
79  //
80  // service functions
81  //
82 
83  virtual void do_initializer(
84  exprt &initializer,
85  const typet &type,
86  bool force_constant);
87 
88  virtual exprt do_initializer_rec(
89  const exprt &value,
90  const typet &type,
91  bool force_constant);
92 
93  virtual exprt do_initializer_list(
94  const exprt &value,
95  const typet &type,
96  bool force_constant);
97 
98  virtual exprt::operandst::const_iterator do_designated_initializer(
99  exprt &result,
100  designatort &designator,
101  const exprt &initializer_list,
102  exprt::operandst::const_iterator init_it,
103  bool force_constant);
104 
105  designatort make_designator(const typet &type, const exprt &src);
106  void designator_enter(const typet &type, designatort &designator); // go down
107  void increment_designator(designatort &designator);
108 
109  // typecasts
110 
112 
113  virtual void implicit_typecast(exprt &expr, const typet &type);
114  virtual void implicit_typecast_arithmetic(exprt &expr);
115  virtual void implicit_typecast_arithmetic(exprt &expr1, exprt &expr2);
116 
117  virtual void implicit_typecast_bool(exprt &expr)
118  {
119  implicit_typecast(expr, bool_typet());
120  }
121 
122  // code
123  virtual void start_typecheck_code();
124  virtual void typecheck_code(codet &code);
125 
126  virtual void typecheck_assign(codet &expr);
127  virtual void typecheck_asm(codet &code);
128  virtual void typecheck_block(code_blockt &code);
129  virtual void typecheck_break(codet &code);
130  virtual void typecheck_continue(codet &code);
131  virtual void typecheck_decl(codet &code);
132  virtual void typecheck_expression(codet &code);
133  virtual void typecheck_for(codet &code);
134  virtual void typecheck_goto(code_gotot &code);
135  virtual void typecheck_ifthenelse(code_ifthenelset &code);
136  virtual void typecheck_label(code_labelt &code);
137  virtual void typecheck_switch_case(code_switch_caset &code);
138  virtual void typecheck_gcc_computed_goto(codet &code);
139  virtual void typecheck_gcc_switch_case_range(codet &code);
140  virtual void typecheck_gcc_local_label(codet &code);
141  virtual void typecheck_return(codet &code);
142  virtual void typecheck_switch(code_switcht &code);
143  virtual void typecheck_while(code_whilet &code);
144  virtual void typecheck_dowhile(code_dowhilet &code);
145  virtual void typecheck_start_thread(codet &code);
146  virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
147 
153 
154  // to check that all labels used are also defined
155  std::map<irep_idt, source_locationt> labels_defined, labels_used;
156 
157  // expressions
158  virtual void typecheck_expr_builtin_va_arg(exprt &expr);
159  virtual void typecheck_expr_builtin_offsetof(exprt &expr);
160  virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
161  virtual void typecheck_expr_main(exprt &expr);
162  virtual void typecheck_expr_operands(exprt &expr);
163  virtual void typecheck_expr_comma(exprt &expr);
164  virtual void typecheck_expr_constant(exprt &expr);
165  virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
166  virtual void typecheck_expr_unary_arithmetic(exprt &expr);
167  virtual void typecheck_expr_unary_boolean(exprt &expr);
168  virtual void typecheck_expr_binary_arithmetic(exprt &expr);
169  virtual void typecheck_expr_shifts(shift_exprt &expr);
170  virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
171  virtual void typecheck_arithmetic_pointer(const exprt &expr);
172  virtual void typecheck_expr_binary_boolean(exprt &expr);
173  virtual void typecheck_expr_trinary(if_exprt &expr);
174  virtual void typecheck_expr_address_of(exprt &expr);
175  virtual void typecheck_expr_dereference(exprt &expr);
176  virtual void typecheck_expr_member(exprt &expr);
177  virtual void typecheck_expr_ptrmember(exprt &expr);
178  virtual void typecheck_expr_rel(binary_relation_exprt &expr);
180  virtual void adjust_float_rel(exprt &expr);
181  static void add_rounding_mode(exprt &);
182  virtual void typecheck_expr_index(exprt &expr);
183  virtual void typecheck_expr_typecast(exprt &expr);
184  virtual void typecheck_expr_symbol(exprt &expr);
185  virtual void typecheck_expr_sizeof(exprt &expr);
186  virtual void typecheck_expr_alignof(exprt &expr);
187  virtual void typecheck_expr_function_identifier(exprt &expr);
189  side_effect_exprt &expr);
194  side_effect_exprt &expr);
198 
199  virtual void make_index_type(exprt &expr);
200  virtual void make_constant(exprt &expr);
201  virtual void make_constant_index(exprt &expr);
202 
203  virtual bool gcc_types_compatible_p(const typet &, const typet &);
204 
205  // types
206  virtual void typecheck_type(typet &type);
207  virtual void typecheck_compound_type(struct_union_typet &type);
208  virtual void typecheck_compound_body(struct_union_typet &type);
209  virtual void typecheck_c_enum_type(typet &type);
210  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
211  virtual void typecheck_code_type(code_typet &type);
212  virtual void typecheck_typedef_type(typet &type);
213  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
214  virtual void typecheck_typeof_type(typet &type);
215  virtual void typecheck_array_type(array_typet &type);
216  virtual void typecheck_vector_type(vector_typet &type);
217  virtual void typecheck_custom_type(typet &type);
218  virtual void adjust_function_parameter(typet &type) const;
219  virtual bool is_complete_type(const typet &type) const;
220 
222  const mp_integer &min, const mp_integer &max) const;
223 
225  const mp_integer &min, const mp_integer &max,
226  bool is_packed) const;
227 
229  {
230  typet result(ID_already_typechecked);
231  result.subtype().swap(dest);
232  result.swap(dest);
233  }
234 
235  // this cleans expressions in array types
236  std::list<codet> clean_code;
237 
238  // environment
239  void add_argc_argv(const symbolt &main_symbol);
240 
241  // symbol table management
242  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
243  void move_symbol(symbolt &symbol)
244  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
245 
246  // top-level stuff
248  void typecheck_symbol(symbolt &symbol);
249  void typecheck_new_symbol(symbolt &symbol);
250  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
252  symbolt &old_symbol, symbolt &new_symbol);
253  void typecheck_function_body(symbolt &symbol);
254 
255  virtual void do_initializer(symbolt &symbol);
256 
257  static bool is_numeric_type(const typet &src)
258  {
259  return src.id()==ID_complex ||
260  src.id()==ID_unsignedbv ||
261  src.id()==ID_signedbv ||
262  src.id()==ID_floatbv ||
263  src.id()==ID_fixedbv ||
264  src.id()==ID_c_bool ||
265  src.id()==ID_bool ||
266  src.id()==ID_c_enum_tag ||
267  src.id()==ID_c_bit_field ||
268  src.id()==ID_integer ||
269  src.id()==ID_real;
270  }
271 
272  typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
274 
275  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
276 };
277 
278 #endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H
c_typecheck_baset::do_initializer
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
Definition: c_typecheck_initializer.cpp:26
c_typecheck_baset::typecheck_expr_side_effect
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:1863
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
c_typecheck_baset::typecheck_new_symbol
void typecheck_new_symbol(symbolt &symbol)
Definition: c_typecheck_base.cpp:141
c_typecheck_baset
Definition: c_typecheck_base.h:25
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
c_typecheck_baset::implicit_typecast_arithmetic
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecheck_typecast.cpp:61
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
c_typecheck_baset::typecheck_asm
virtual void typecheck_asm(codet &code)
Definition: c_typecheck_code.cpp:135
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1326
ansi_c_declaration.h
c_typecheck_baset::do_designated_initializer
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)
Definition: c_typecheck_initializer.cpp:353
c_typecheck_baset::gcc_vector_types_compatible
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
Definition: c_typecheck_expr.cpp:2947
c_typecheck_baset::add_argc_argv
void add_argc_argv(const symbolt &main_symbol)
Definition: c_typecheck_argc_argv.cpp:16
c_typecheck_baset::typecheck_array_type
virtual void typecheck_array_type(array_typet &type)
Definition: c_typecheck_type.cpp:508
c_typecheck_baset::current_symbol
symbolt current_symbol
Definition: c_typecheck_base.h:70
code_whilet
codet representing a while statement.
Definition: std_code.h:767
c_typecheck_baset::typecheck_expr_builtin_offsetof
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
Definition: c_typecheck_expr.cpp:562
c_typecheck_baset::typecheck_expr_shifts
virtual void typecheck_expr_shifts(shift_exprt &expr)
Definition: c_typecheck_expr.cpp:3093
c_typecheck_baset::typecheck_while
virtual void typecheck_while(code_whilet &code)
Definition: c_typecheck_code.cpp:716
c_typecheck_baset::typecheck_gcc_switch_case_range
virtual void typecheck_gcc_switch_case_range(codet &code)
Definition: c_typecheck_code.cpp:518
c_typecheck_baset::do_special_functions
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
Definition: c_typecheck_expr.cpp:2072
c_typecheck_baset::typecheck_vector_type
virtual void typecheck_vector_type(vector_typet &type)
Definition: c_typecheck_type.cpp:658
typet
The type of an expression, extends irept.
Definition: type.h:27
c_typecheck_baset::enum_constant_type
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
Definition: c_typecheck_type.cpp:1044
c_typecheck_baset::adjust_float_rel
virtual void adjust_float_rel(exprt &expr)
Definition: c_typecheck_expr.cpp:1327
c_typecheck_baset::typecheck_declaration
void typecheck_declaration(ansi_c_declarationt &)
Definition: c_typecheck_base.cpp:654
c_typecheck_baset::typecheck_break
virtual void typecheck_break(codet &code)
Definition: c_typecheck_code.cpp:203
c_typecheck_baset::to_string
virtual std::string to_string(const exprt &expr)
Definition: c_typecheck_base.cpp:23
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:114
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
c_typecheck_baset::add_rounding_mode
static void add_rounding_mode(exprt &)
Definition: c_typecheck_expr.cpp:54
c_typecheck_baset::typecheck_return
virtual void typecheck_return(codet &code)
Definition: c_typecheck_code.cpp:639
c_typecheck_baset::typecheck_function_call_arguments
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
Definition: c_typecheck_expr.cpp:2799
c_typecheck_baset::typecheck_side_effect_statement_expression
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:891
c_typecheck_baset::typecheck_expr_symbol
virtual void typecheck_expr_symbol(exprt &expr)
Definition: c_typecheck_expr.cpp:787
exprt
Base class for all expressions.
Definition: expr.h:54
c_typecheck_baset::typecheck_expr_pointer_arithmetic
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
Definition: c_typecheck_expr.cpp:3177
c_typecheck_baset::asm_label_mapt
std::unordered_map< irep_idt, irep_idt > asm_label_mapt
Definition: c_typecheck_base.h:272
c_typecheck_baset::typecheck_expr_rel_vector
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
Definition: c_typecheck_expr.cpp:1447
designatort
Definition: designator.h:20
c_typecheck_baset::typecheck_expr_address_of
virtual void typecheck_expr_address_of(exprt &expr)
Definition: c_typecheck_expr.cpp:1732
c_typecheck_baset::typecheck_expr_alignof
virtual void typecheck_expr_alignof(exprt &expr)
Definition: c_typecheck_expr.cpp:1039
c_typecheck_baset::enum_underlying_type
typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
Definition: c_typecheck_type.cpp:1076
vector_typet
The vector type.
Definition: std_types.h:1755
c_typecheck_baset::move_symbol
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
Definition: c_typecheck_base.cpp:33
bool_typet
The Boolean type.
Definition: std_types.h:28
c_typecheck_baset::typecheck_type
virtual void typecheck_type(typet &type)
Definition: c_typecheck_type.cpp:29
c_typecheck_baset::typecheck_side_effect_function_call
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
Definition: c_typecheck_expr.cpp:1954
c_typecheck_baset::typecheck_c_bit_field_type
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
Definition: c_typecheck_type.cpp:1376
c_typecheck_baset::typecheck_spec_expr
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:782
c_typecheck_baset::typecheck_expr_binary_arithmetic
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
Definition: c_typecheck_expr.cpp:2974
namespace.h
c_typecheck_baset::typecheck_expr_binary_boolean
virtual void typecheck_expr_binary_boolean(exprt &expr)
Definition: c_typecheck_expr.cpp:3267
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:614
c_typecheck_baset::clean_code
std::list< codet > clean_code
Definition: c_typecheck_base.h:236
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:3482
c_typecheck_baset::do_initializer_list
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
Definition: c_typecheck_initializer.cpp:830
c_typecheck_baset::typecheck_expr_operands
virtual void typecheck_expr_operands(exprt &expr)
Definition: c_typecheck_expr.cpp:717
c_typecheck_baset::typecheck_redefinition_non_type
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
Definition: c_typecheck_base.cpp:254
c_typecheck_baset::typecheck_expr_member
virtual void typecheck_expr_member(exprt &expr)
Definition: c_typecheck_expr.cpp:1513
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
c_typecheck_baset::typecheck_continue
virtual void typecheck_continue(codet &code)
Definition: c_typecheck_code.cpp:213
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:68
c_typecheck_baset::asm_label_map
asm_label_mapt asm_label_map
Definition: c_typecheck_base.h:273
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:829
c_typecheck_baset::typecheck_expr_rel
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
Definition: c_typecheck_expr.cpp:1341
messaget::result
mstreamt & result() const
Definition: message.h:396
c_typecheck_baset::typecheck_expr_unary_arithmetic
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
Definition: c_typecheck_expr.cpp:2886
c_typecheck_baset::typecheck_function_body
void typecheck_function_body(symbolt &symbol)
Definition: c_typecheck_base.cpp:516
c_bit_field_typet
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: std_types.h:1462
c_typecheck_baset::implicit_typecast_bool
virtual void implicit_typecast_bool(exprt &expr)
Definition: c_typecheck_base.h:117
c_typecheck_baset::typecheck_expr_function_identifier
virtual void typecheck_expr_function_identifier(exprt &expr)
Definition: c_typecheck_expr.cpp:1852
c_typecheck_baset::typecheck_label
virtual void typecheck_label(code_labelt &code)
Definition: c_typecheck_code.cpp:474
c_typecheck_baset::typecheck_expr_dereference
virtual void typecheck_expr_dereference(exprt &expr)
Definition: c_typecheck_expr.cpp:1809
typecheck.h
code_gotot
codet representation of a goto statement.
Definition: std_code.h:983
c_typecheck_baset::move_symbol
void move_symbol(symbolt &symbol)
Definition: c_typecheck_base.h:243
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1256
c_typecheck_baset::typecheck_symbol
void typecheck_symbol(symbolt &symbol)
Definition: c_typecheck_base.cpp:47
c_typecheck_baset::case_is_allowed
bool case_is_allowed
Definition: c_typecheck_base.h:150
c_typecheck_baset::continue_is_allowed
bool continue_is_allowed
Definition: c_typecheck_base.h:149
c_typecheck_baset::is_complete_type
virtual bool is_complete_type(const typet &type) const
Definition: c_typecheck_code.cpp:342
std_types.h
c_typecheck_baset::typecheck_c_enum_tag_type
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
Definition: c_typecheck_type.cpp:1317
c_typecheck_baset::make_already_typechecked
void make_already_typechecked(typet &dest)
Definition: c_typecheck_base.h:228
c_typecheck_baset::typecheck_expression
virtual void typecheck_expression(codet &code)
Definition: c_typecheck_code.cpp:369
c_typecheck_baset::typecheck_expr_unary_boolean
virtual void typecheck_expr_unary_boolean(exprt &expr)
Definition: c_typecheck_expr.cpp:2925
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:67
c_typecheck_baset::gcc_types_compatible_p
virtual bool gcc_types_compatible_p(const typet &, const typet &)
Definition: c_typecheck_expr.cpp:88
c_typecheck_baset::typecheck_goto
virtual void typecheck_goto(code_gotot &code)
Definition: c_typecheck_code.cpp:551
c_typecheck_baset::typecheck_code
virtual void typecheck_code(codet &code)
Definition: c_typecheck_code.cpp:24
c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:1701
code_typet
Base type of functions.
Definition: std_types.h:751
c_typecheck_baset::typecheck_arithmetic_pointer
virtual void typecheck_arithmetic_pointer(const exprt &expr)
Definition: c_typecheck_expr.cpp:3162
c_typecheck_baset::make_constant_index
virtual void make_constant_index(exprt &expr)
Definition: c_typecheck_expr.cpp:3503
irept::id
const irep_idt & id() const
Definition: irep.h:259
message_handlert
Definition: message.h:24
c_typecheck_baset::typecheck_expr_trinary
virtual void typecheck_expr_trinary(if_exprt &expr)
Definition: c_typecheck_expr.cpp:1609
c_typecheck_baset::typecheck_typedef_type
virtual void typecheck_typedef_type(typet &type)
Definition: c_typecheck_type.cpp:1493
c_typecheck_baset::typecheck_typeof_type
virtual void typecheck_typeof_type(typet &type)
Definition: c_typecheck_type.cpp:1456
c_typecheck_baset::typecheck_redefinition_type
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
Definition: c_typecheck_base.cpp:171
std_code.h
c_typecheck_baset::typecheck_side_effect_assignment
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:3288
c_typecheck_baset::parameter_map
id_type_mapt parameter_map
Definition: c_typecheck_base.h:73
c_typecheck_baset::typecheck_dowhile
virtual void typecheck_dowhile(code_dowhilet &code)
Definition: c_typecheck_code.cpp:749
c_typecheck_baset::designator_enter
void designator_enter(const typet &type, designatort &designator)
Definition: c_typecheck_initializer.cpp:260
c_typecheck_baset::labels_used
std::map< irep_idt, source_locationt > labels_used
Definition: c_typecheck_base.h:155
c_typecheck_baset::typecheck_expr_ptrmember
virtual void typecheck_expr_ptrmember(exprt &expr)
Definition: c_typecheck_expr.cpp:1473
c_typecheck_baset::typecheck_switch
virtual void typecheck_switch(code_switcht &code)
Definition: c_typecheck_code.cpp:685
c_typecheck_baset::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: c_typecheck_expr.cpp:36
c_typecheck_baset::switch_op_type
typet switch_op_type
Definition: c_typecheck_base.h:151
c_typecheck_baset::break_is_allowed
bool break_is_allowed
Definition: c_typecheck_base.h:148
c_typecheck_baset::typecheck_for
virtual void typecheck_for(codet &code)
Definition: c_typecheck_code.cpp:383
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2866
ansi_c_declarationt
Definition: ansi_c_declaration.h:72
c_typecheck_baset::c_typecheck_baset
c_typecheck_baset(symbol_tablet &_symbol_table, const std::string &_module, message_handlert &_message_handler)
Definition: c_typecheck_base.h:30
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:711
c_typecheck_baset::typecheck_decl
virtual void typecheck_decl(codet &code)
Definition: c_typecheck_code.cpp:223
c_typecheck_baset::do_initializer_rec
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
Definition: c_typecheck_initializer.cpp:54
c_typecheck_baset::is_numeric_type
static bool is_numeric_type(const typet &src)
Definition: c_typecheck_base.h:257
array_typet
Arrays with given size.
Definition: std_types.h:1000
c_typecheck_baset::typecheck_expr_main
virtual void typecheck_expr_main(exprt &expr)
Definition: c_typecheck_expr.cpp:165
c_typecheck_baset::typecheck
virtual void typecheck()=0
c_typecheck_baset::make_designator
designatort make_designator(const typet &type, const exprt &src)
Definition: c_typecheck_initializer.cpp:686
c_typecheck_baset::labels_defined
std::map< irep_idt, source_locationt > labels_defined
Definition: c_typecheck_base.h:155
code_switcht
codet representing a switch statement.
Definition: std_code.h:705
symbolt
Symbol table entry.
Definition: symbol.h:27
c_typecheck_baset::typecheck_expr_cw_va_arg_typeof
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
Definition: c_typecheck_expr.cpp:545
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
c_typecheck_baset::typecheck_assign
virtual void typecheck_assign(codet &expr)
Definition: c_typecheck_code.cpp:168
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:152
c_typecheck_baset::typecheck_expr_constant
virtual void typecheck_expr_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:2881
c_typecheck_baset::~c_typecheck_baset
virtual ~c_typecheck_baset()
Definition: c_typecheck_base.h:61
c_typecheck_baset::typecheck_custom_type
virtual void typecheck_custom_type(typet &type)
Definition: c_typecheck_type.cpp:307
c_typecheck_baset::typecheck_start_thread
virtual void typecheck_start_thread(codet &code)
Definition: c_typecheck_code.cpp:627
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:582
c_typecheck_baset::typecheck_c_enum_type
virtual void typecheck_c_enum_type(typet &type)
Definition: c_typecheck_type.cpp:1134
c_typecheck_baset::increment_designator
void increment_designator(designatort &designator)
Definition: c_typecheck_initializer.cpp:638
c_typecheck_baset::start_typecheck_code
virtual void start_typecheck_code()
Definition: c_typecheck_code.cpp:19
c_typecheck_baset::typecheck_switch_case
virtual void typecheck_switch_case(code_switch_caset &code)
Definition: c_typecheck_code.cpp:482
c_typecheck_baset::typecheck_compound_type
virtual void typecheck_compound_type(struct_union_typet &type)
Definition: c_typecheck_type.cpp:739
typecheckt
Definition: typecheck.h:16
c_typecheck_baset::typecheck_gcc_computed_goto
virtual void typecheck_gcc_computed_goto(codet &code)
Definition: c_typecheck_code.cpp:557
symbol_table.h
Author: Diffblue Ltd.
designator.h
c_typecheck_baset::typecheck_code_type
virtual void typecheck_code_type(code_typet &type)
Definition: c_typecheck_type.cpp:409
c_typecheck_baset::typecheck_expr_sizeof
virtual void typecheck_expr_sizeof(exprt &expr)
Definition: c_typecheck_expr.cpp:960
std_expr.h
c_typecheck_baset::mode
const irep_idt mode
Definition: c_typecheck_base.h:69
c_typecheck_baset::typecheck_gcc_local_label
virtual void typecheck_gcc_local_label(codet &code)
Definition: c_typecheck_code.cpp:545
c_typecheck_baset::id_type_mapt
std::unordered_map< irep_idt, typet > id_type_mapt
Definition: c_typecheck_base.h:72
c_typecheck_baset::c_typecheck_baset
c_typecheck_baset(symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2, const std::string &_module, message_handlert &_message_handler)
Definition: c_typecheck_base.h:45
c_typecheck_baset::apply_asm_label
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
Definition: c_typecheck_base.cpp:586
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
c_typecheck_baset::typecheck_compound_body
virtual void typecheck_compound_body(struct_union_typet &type)
Definition: c_typecheck_type.cpp:867
c_typecheck_baset::typecheck_expr_index
virtual void typecheck_expr_index(exprt &expr)
Definition: c_typecheck_expr.cpp:1260
c_typecheck_baset::make_index_type
virtual void make_index_type(exprt &expr)
Definition: c_typecheck_expr.cpp:1255
c_typecheck_baset::typecheck_block
virtual void typecheck_block(code_blockt &code)
Definition: c_typecheck_code.cpp:184
c_typecheck_baset::typecheck_expr_builtin_va_arg
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
Definition: c_typecheck_expr.cpp:504
c_typecheck_baset::implicit_typecast
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecheck_typecast.cpp:13
c_typecheck_baset::adjust_function_parameter
virtual void adjust_function_parameter(typet &type) const
Definition: c_typecheck_type.cpp:1542
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
c_typecheck_baset::typecheck_expr_comma
virtual void typecheck_expr_comma(exprt &expr)
Definition: c_typecheck_expr.cpp:488
c_typecheck_baset::typecheck_expr_typecast
virtual void typecheck_expr_typecast(exprt &expr)
Definition: c_typecheck_expr.cpp:1061