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(code_asmt &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);
140  virtual void typecheck_gcc_local_label(codet &code);
141  virtual void typecheck_return(code_returnt &code);
142  virtual void typecheck_switch(codet &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(binary_relation_exprt &);
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);
199  const irep_idt &identifier,
200  const exprt::operandst &arguments,
201  const source_locationt &source_location);
203  const irep_idt &identifier,
204  const symbol_exprt &function_symbol);
205 
206  virtual void make_index_type(exprt &expr);
207  virtual void make_constant(exprt &expr);
208  virtual void make_constant_index(exprt &expr);
209 
210  virtual bool gcc_types_compatible_p(const typet &, const typet &);
211 
212  // types
213  virtual void typecheck_type(typet &type);
214  virtual void typecheck_compound_type(struct_union_typet &type);
215  virtual void typecheck_compound_body(struct_union_typet &type);
216  virtual void typecheck_c_enum_type(typet &type);
217  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
218  virtual void typecheck_code_type(code_typet &type);
219  virtual void typecheck_typedef_type(typet &type);
220  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
221  virtual void typecheck_typeof_type(typet &type);
222  virtual void typecheck_array_type(array_typet &type);
223  virtual void typecheck_vector_type(typet &type);
224  virtual void typecheck_custom_type(typet &type);
225  virtual void adjust_function_parameter(typet &type) const;
226  virtual bool is_complete_type(const typet &type) const;
227 
229  const mp_integer &min, const mp_integer &max) const;
230 
232  const mp_integer &min,
233  const mp_integer &max,
234  bool is_packed) const;
235 
236  // this cleans expressions in array types
237  std::list<codet> clean_code;
238 
239  // symbol table management
240  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
241  void move_symbol(symbolt &symbol)
242  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
243 
244  // top-level stuff
246  void typecheck_symbol(symbolt &symbol);
247  void typecheck_new_symbol(symbolt &symbol);
248  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
250  symbolt &old_symbol, symbolt &new_symbol);
251  void typecheck_function_body(symbolt &symbol);
252 
253  virtual void do_initializer(symbolt &symbol);
254 
255  static bool is_numeric_type(const typet &src)
256  {
257  return src.id()==ID_complex ||
258  src.id()==ID_unsignedbv ||
259  src.id()==ID_signedbv ||
260  src.id()==ID_floatbv ||
261  src.id()==ID_fixedbv ||
262  src.id()==ID_c_bool ||
263  src.id()==ID_bool ||
264  src.id()==ID_c_enum_tag ||
265  src.id()==ID_c_bit_field ||
266  src.id()==ID_integer ||
267  src.id()==ID_real;
268  }
269 
270  typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
272 
273  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
274 };
275 
277 {
278 public:
280  : expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
281  {
282  }
283 
284  static void make_already_typechecked(exprt &expr)
285  {
287  expr.swap(a);
288  }
289 
291  {
292  return op0();
293  }
294 };
295 
297 {
298 public:
300  : type_with_subtypet(ID_already_typechecked, std::move(type))
301  {
302  }
303 
304  static void make_already_typechecked(typet &type)
305  {
307  type.swap(a);
308  }
309 
311  {
312  return subtype();
313  }
314 };
315 
317 {
318  PRECONDITION(expr.id() == ID_already_typechecked);
319  PRECONDITION(expr.operands().size() == 1);
320 
321  return static_cast<already_typechecked_exprt &>(expr);
322 }
323 
325 {
326  PRECONDITION(type.id() == ID_already_typechecked);
327  PRECONDITION(type.has_subtype());
328 
329  return static_cast<already_typechecked_typet &>(type);
330 }
331 
332 #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:25
c_typecheck_baset::typecheck_expr_side_effect
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:1762
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
c_typecheck_baset::typecheck_new_symbol
void typecheck_new_symbol(symbolt &symbol)
Definition: c_typecheck_base.cpp:136
c_typecheck_baset
Definition: c_typecheck_base.h:28
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:173
c_typecheck_baset::implicit_typecast_arithmetic
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecheck_typecast.cpp:50
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
typet::subtype
const typet & subtype() const
Definition: type.h:47
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1449
ansi_c_declaration.h
c_typecheck_baset::typecheck_vector_type
virtual void typecheck_vector_type(typet &type)
Definition: c_typecheck_type.cpp:652
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:358
c_typecheck_baset::gcc_vector_types_compatible
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
Definition: c_typecheck_expr.cpp:2938
c_typecheck_baset::typecheck_array_type
virtual void typecheck_array_type(array_typet &type)
Definition: c_typecheck_type.cpp:519
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:899
c_typecheck_baset::typecheck_expr_builtin_offsetof
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
Definition: c_typecheck_expr.cpp:546
c_typecheck_baset::typecheck_expr_shifts
virtual void typecheck_expr_shifts(shift_exprt &expr)
Definition: c_typecheck_expr.cpp:3079
c_typecheck_baset::typecheck_while
virtual void typecheck_while(code_whilet &code)
Definition: c_typecheck_code.cpp:731
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1679
c_typecheck_baset::do_special_functions
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
Definition: c_typecheck_expr.cpp:2029
typet
The type of an expression, extends irept.
Definition: type.h:29
to_already_typechecked_expr
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
Definition: c_typecheck_base.h:316
c_typecheck_baset::enum_constant_type
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
Definition: c_typecheck_type.cpp:1048
c_typecheck_baset::typecheck_declaration
void typecheck_declaration(ansi_c_declarationt &)
Definition: c_typecheck_base.cpp:625
c_typecheck_baset::typecheck_break
virtual void typecheck_break(codet &code)
Definition: c_typecheck_code.cpp:206
c_typecheck_baset::to_string
virtual std::string to_string(const exprt &expr)
Definition: c_typecheck_base.cpp:24
c_typecheck_baset::adjust_float_rel
virtual void adjust_float_rel(binary_relation_exprt &)
Definition: c_typecheck_expr.cpp:1275
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2127
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2993
c_typecheck_baset::add_rounding_mode
static void add_rounding_mode(exprt &)
Definition: c_typecheck_expr.cpp:54
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:2810
already_typechecked_typet
Definition: c_typecheck_base.h:297
c_typecheck_baset::typecheck_side_effect_statement_expression
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:882
c_typecheck_baset::typecheck_expr_symbol
virtual void typecheck_expr_symbol(exprt &expr)
Definition: c_typecheck_expr.cpp:779
c_typecheck_baset::enum_underlying_type
bitvector_typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
Definition: c_typecheck_type.cpp:1080
exprt
Base class for all expressions.
Definition: expr.h:53
c_typecheck_baset::typecheck_expr_pointer_arithmetic
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
Definition: c_typecheck_expr.cpp:3171
c_typecheck_baset::asm_label_mapt
std::unordered_map< irep_idt, irep_idt > asm_label_mapt
Definition: c_typecheck_base.h:270
c_typecheck_baset::typecheck_expr_rel_vector
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
Definition: c_typecheck_expr.cpp:1389
designatort
Definition: designator.h:21
c_typecheck_baset::typecheck_expr_address_of
virtual void typecheck_expr_address_of(exprt &expr)
Definition: c_typecheck_expr.cpp:1646
c_typecheck_baset::typecheck_expr_alignof
virtual void typecheck_expr_alignof(exprt &expr)
Definition: c_typecheck_expr.cpp:1007
vector_typet
The vector type.
Definition: std_types.h:1750
c_typecheck_baset::move_symbol
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
Definition: c_typecheck_base.cpp:34
bool_typet
The Boolean type.
Definition: std_types.h:37
code_gcc_switch_case_ranget
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1523
c_typecheck_baset::typecheck_type
virtual void typecheck_type(typet &type)
Definition: c_typecheck_type.cpp:31
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:1850
type_with_subtypet
Type with a single subtype.
Definition: type.h:146
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:1394
c_typecheck_baset::typecheck_spec_expr
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:797
c_typecheck_baset::typecheck_expr_binary_arithmetic
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
Definition: c_typecheck_expr.cpp:2966
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
c_typecheck_baset::typecheck_expr_binary_boolean
virtual void typecheck_expr_binary_boolean(exprt &expr)
Definition: c_typecheck_expr.cpp:3258
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:749
c_typecheck_baset::clean_code
std::list< codet > clean_code
Definition: c_typecheck_base.h:237
to_already_typechecked_type
already_typechecked_typet & to_already_typechecked_type(typet &type)
Definition: c_typecheck_base.h:324
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:3448
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:847
c_typecheck_baset::typecheck_expr_operands
virtual void typecheck_expr_operands(exprt &expr)
Definition: c_typecheck_expr.cpp:705
c_typecheck_baset::typecheck_redefinition_non_type
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
Definition: c_typecheck_base.cpp:258
c_typecheck_baset::typecheck_expr_member
virtual void typecheck_expr_member(exprt &expr)
Definition: c_typecheck_expr.cpp:1448
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
already_typechecked_exprt::already_typechecked_exprt
already_typechecked_exprt(exprt expr)
Definition: c_typecheck_base.h:279
c_typecheck_baset::typecheck_continue
virtual void typecheck_continue(codet &code)
Definition: c_typecheck_code.cpp:216
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:271
expr_protectedt::op0
exprt & op0()
Definition: expr.h:101
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:961
c_typecheck_baset::typecheck_expr_rel
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
Definition: c_typecheck_expr.cpp:1287
messaget::result
mstreamt & result() const
Definition: message.h:395
c_typecheck_baset::typecheck_asm
virtual void typecheck_asm(code_asmt &code)
Definition: c_typecheck_code.cpp:137
c_typecheck_baset::typecheck_expr_unary_arithmetic
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
Definition: c_typecheck_expr.cpp:2896
already_typechecked_exprt::make_already_typechecked
static void make_already_typechecked(exprt &expr)
Definition: c_typecheck_base.h:284
c_typecheck_baset::typecheck_function_body
void typecheck_function_body(symbolt &symbol)
Definition: c_typecheck_base.cpp:499
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:1443
c_typecheck_baset::implicit_typecast_bool
virtual void implicit_typecast_bool(exprt &expr)
Definition: c_typecheck_base.h:117
c_typecheck_baset::instantiate_gcc_polymorphic_builtin
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1212
c_typecheck_baset::typecheck_expr_function_identifier
virtual void typecheck_expr_function_identifier(exprt &expr)
Definition: c_typecheck_expr.cpp:1751
already_typechecked_exprt::get_expr
exprt & get_expr()
Definition: c_typecheck_base.h:290
c_typecheck_baset::typecheck_label
virtual void typecheck_label(code_labelt &code)
Definition: c_typecheck_code.cpp:476
c_typecheck_baset::typecheck_expr_dereference
virtual void typecheck_expr_dereference(exprt &expr)
Definition: c_typecheck_expr.cpp:1715
typecheck.h
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1130
c_typecheck_baset::move_symbol
void move_symbol(symbolt &symbol)
Definition: c_typecheck_base.h:241
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1378
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
c_typecheck_baset::typecheck_symbol
void typecheck_symbol(symbolt &symbol)
Definition: c_typecheck_base.cpp:48
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:1336
c_typecheck_baset::typecheck_expression
virtual void typecheck_expression(codet &code)
Definition: c_typecheck_code.cpp:371
c_typecheck_baset::typecheck_expr_unary_boolean
virtual void typecheck_expr_unary_boolean(exprt &expr)
Definition: c_typecheck_expr.cpp:2926
c_typecheck_baset::typecheck_gcc_polymorphic_builtin
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:481
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:89
already_typechecked_typet::already_typechecked_typet
already_typechecked_typet(typet type)
Definition: c_typecheck_base.h:299
c_typecheck_baset::typecheck_goto
virtual void typecheck_goto(code_gotot &code)
Definition: c_typecheck_code.cpp:545
c_typecheck_baset::typecheck_code
virtual void typecheck_code(codet &code)
Definition: c_typecheck_code.cpp:26
irept::swap
void swap(irept &irep)
Definition: irep.h:463
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:1618
code_typet
Base type of functions.
Definition: std_types.h:736
c_typecheck_baset::typecheck_arithmetic_pointer
virtual void typecheck_arithmetic_pointer(const exprt &expr)
Definition: c_typecheck_expr.cpp:3146
c_typecheck_baset::make_constant_index
virtual void make_constant_index(exprt &expr)
Definition: c_typecheck_expr.cpp:3469
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:27
c_typecheck_baset::typecheck_expr_trinary
virtual void typecheck_expr_trinary(if_exprt &expr)
Definition: c_typecheck_expr.cpp:1527
c_typecheck_baset::typecheck_typedef_type
virtual void typecheck_typedef_type(typet &type)
Definition: c_typecheck_type.cpp:1510
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
c_typecheck_baset::typecheck_typeof_type
virtual void typecheck_typeof_type(typet &type)
Definition: c_typecheck_type.cpp:1474
c_typecheck_baset::typecheck_redefinition_type
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
Definition: c_typecheck_base.cpp:164
c_typecheck_baset::typecheck_switch
virtual void typecheck_switch(codet &code)
Definition: c_typecheck_code.cpp:668
c_typecheck_baset::typecheck_return
virtual void typecheck_return(code_returnt &code)
Definition: c_typecheck_code.cpp:631
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
c_typecheck_baset::typecheck_side_effect_assignment
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:3272
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:764
c_typecheck_baset::designator_enter
void designator_enter(const typet &type, designatort &designator)
Definition: c_typecheck_initializer.cpp:266
already_typechecked_typet::get_type
typet & get_type()
Definition: c_typecheck_base.h:310
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:1414
c_typecheck_baset::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: c_typecheck_expr.cpp:39
c_typecheck_baset::switch_op_type
typet switch_op_type
Definition: c_typecheck_base.h:151
source_locationt
Definition: source_location.h:20
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:385
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2525
ansi_c_declarationt
Definition: ansi_c_declaration.h:73
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:696
c_typecheck_baset::typecheck_decl
virtual void typecheck_decl(codet &code)
Definition: c_typecheck_code.cpp:226
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:53
c_typecheck_baset::typecheck_gcc_switch_case_range
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &)
Definition: c_typecheck_code.cpp:520
c_typecheck_baset::is_numeric_type
static bool is_numeric_type(const typet &src)
Definition: c_typecheck_base.h:255
array_typet
Arrays with given size.
Definition: std_types.h:965
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1313
c_typecheck_baset::typecheck_expr_main
virtual void typecheck_expr_main(exprt &expr)
Definition: c_typecheck_expr.cpp:166
c_typecheck_baset::typecheck
virtual void typecheck()=0
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1030
c_typecheck_baset::make_designator
designatort make_designator(const typet &type, const exprt &src)
Definition: c_typecheck_initializer.cpp:699
c_typecheck_baset::labels_defined
std::map< irep_idt, source_locationt > labels_defined
Definition: c_typecheck_base.h:155
symbolt
Symbol table entry.
Definition: symbol.h:28
c_typecheck_baset::typecheck_expr_cw_va_arg_typeof
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
Definition: c_typecheck_expr.cpp:529
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
c_typecheck_baset::typecheck_assign
virtual void typecheck_assign(codet &expr)
Definition: c_typecheck_code.cpp:171
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:2891
c_typecheck_baset::~c_typecheck_baset
virtual ~c_typecheck_baset()
Definition: c_typecheck_base.h:61
already_typechecked_exprt
Definition: c_typecheck_base.h:277
c_typecheck_baset::typecheck_custom_type
virtual void typecheck_custom_type(typet &type)
Definition: c_typecheck_type.cpp:319
c_typecheck_baset::typecheck_start_thread
virtual void typecheck_start_thread(codet &code)
Definition: c_typecheck_code.cpp:619
already_typechecked_typet::make_already_typechecked
static void make_already_typechecked(typet &type)
Definition: c_typecheck_base.h:304
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:574
c_typecheck_baset::typecheck_c_enum_type
virtual void typecheck_c_enum_type(typet &type)
Definition: c_typecheck_type.cpp:1138
c_typecheck_baset::increment_designator
void increment_designator(designatort &designator)
Definition: c_typecheck_initializer.cpp:645
exprt::operands
operandst & operands()
Definition: expr.h:95
c_typecheck_baset::start_typecheck_code
virtual void start_typecheck_code()
Definition: c_typecheck_code.cpp:21
c_typecheck_baset::typecheck_switch_case
virtual void typecheck_switch_case(code_switch_caset &code)
Definition: c_typecheck_code.cpp:484
c_typecheck_baset::typecheck_compound_type
virtual void typecheck_compound_type(struct_union_typet &type)
Definition: c_typecheck_type.cpp:747
typecheckt
Definition: typecheck.h:17
c_typecheck_baset::typecheck_gcc_computed_goto
virtual void typecheck_gcc_computed_goto(codet &code)
Definition: c_typecheck_code.cpp:551
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:421
c_typecheck_baset::typecheck_expr_sizeof
virtual void typecheck_expr_sizeof(exprt &expr)
Definition: c_typecheck_expr.cpp:914
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:539
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:560
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1876
c_typecheck_baset::typecheck_compound_body
virtual void typecheck_compound_body(struct_union_typet &type)
Definition: c_typecheck_type.cpp:872
c_typecheck_baset::typecheck_expr_index
virtual void typecheck_expr_index(exprt &expr)
Definition: c_typecheck_expr.cpp:1217
expr_protectedt
Base class for all expressions.
Definition: expr.h:365
c_typecheck_baset::make_index_type
virtual void make_index_type(exprt &expr)
Definition: c_typecheck_expr.cpp:1212
c_typecheck_baset::typecheck_block
virtual void typecheck_block(code_blockt &code)
Definition: c_typecheck_code.cpp:187
c_typecheck_baset::typecheck_expr_builtin_va_arg
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
Definition: c_typecheck_expr.cpp:488
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:1559
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
c_typecheck_baset::typecheck_expr_comma
virtual void typecheck_expr_comma(exprt &expr)
Definition: c_typecheck_expr.cpp:479
c_typecheck_baset::typecheck_expr_typecast
virtual void typecheck_expr_typecast(exprt &expr)
Definition: c_typecheck_expr.cpp:1029