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  virtual void
148  typecheck_assigns(const code_typet &function_declarator, const irept &spec);
149  virtual void
150  typecheck_assigns(const ansi_c_declaratort &declarator, const exprt &assigns);
151  virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec);
152 
158 
159  // to check that all labels used are also defined
160  std::map<irep_idt, source_locationt> labels_defined, labels_used;
161 
162  // expressions
163  virtual void typecheck_expr_builtin_va_arg(exprt &expr);
164  virtual void typecheck_expr_builtin_offsetof(exprt &expr);
165  virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
166  virtual void typecheck_expr_main(exprt &expr);
167  virtual void typecheck_expr_operands(exprt &expr);
168  virtual void typecheck_expr_comma(exprt &expr);
169  virtual void typecheck_expr_constant(exprt &expr);
170  virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
171  virtual void typecheck_expr_unary_arithmetic(exprt &expr);
172  virtual void typecheck_expr_unary_boolean(exprt &expr);
173  virtual void typecheck_expr_binary_arithmetic(exprt &expr);
174  virtual void typecheck_expr_shifts(shift_exprt &expr);
175  virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
176  virtual void typecheck_arithmetic_pointer(const exprt &expr);
177  virtual void typecheck_expr_binary_boolean(exprt &expr);
178  virtual void typecheck_expr_trinary(if_exprt &expr);
179  virtual void typecheck_expr_address_of(exprt &expr);
180  virtual void typecheck_expr_dereference(exprt &expr);
181  virtual void typecheck_expr_member(exprt &expr);
182  virtual void typecheck_expr_ptrmember(exprt &expr);
183  virtual void typecheck_expr_rel(binary_relation_exprt &expr);
185  virtual void adjust_float_rel(binary_relation_exprt &);
186  static void add_rounding_mode(exprt &);
187  virtual void typecheck_expr_index(exprt &expr);
188  virtual void typecheck_expr_typecast(exprt &expr);
189  virtual void typecheck_expr_symbol(exprt &expr);
190  virtual void typecheck_expr_sizeof(exprt &expr);
191  virtual void typecheck_expr_alignof(exprt &expr);
192  virtual void typecheck_expr_function_identifier(exprt &expr);
194  side_effect_exprt &expr);
199  side_effect_exprt &expr);
204  const irep_idt &identifier,
205  const exprt::operandst &arguments,
206  const source_locationt &source_location);
208  const irep_idt &identifier,
209  const symbol_exprt &function_symbol);
210 
211  virtual void make_index_type(exprt &expr);
212  virtual void make_constant(exprt &expr);
213  virtual void make_constant_index(exprt &expr);
214 
215  virtual bool gcc_types_compatible_p(const typet &, const typet &);
216 
217  // types
218  virtual void typecheck_type(typet &type);
219  virtual void typecheck_compound_type(struct_union_typet &type);
220  virtual void typecheck_compound_body(struct_union_typet &type);
221  virtual void typecheck_c_enum_type(typet &type);
222  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
223  virtual void typecheck_code_type(code_typet &type);
224  virtual void typecheck_typedef_type(typet &type);
225  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
226  virtual void typecheck_typeof_type(typet &type);
227  virtual void typecheck_array_type(array_typet &type);
228  virtual void typecheck_vector_type(typet &type);
229  virtual void typecheck_custom_type(typet &type);
230  virtual void adjust_function_parameter(typet &type) const;
231  virtual bool is_complete_type(const typet &type) const;
232 
234  const mp_integer &min, const mp_integer &max) const;
235 
237  const mp_integer &min,
238  const mp_integer &max,
239  bool is_packed) const;
240 
241  // this cleans expressions in array types
242  std::list<codet> clean_code;
243 
244  // symbol table management
245  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
246  void move_symbol(symbolt &symbol)
247  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
248 
249  // top-level stuff
251  void typecheck_symbol(symbolt &symbol);
252  void typecheck_new_symbol(symbolt &symbol);
253  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
255  symbolt &old_symbol, symbolt &new_symbol);
256  void typecheck_function_body(symbolt &symbol);
257 
258  virtual void do_initializer(symbolt &symbol);
259 
260  static bool is_numeric_type(const typet &src)
261  {
262  return src.id()==ID_complex ||
263  src.id()==ID_unsignedbv ||
264  src.id()==ID_signedbv ||
265  src.id()==ID_floatbv ||
266  src.id()==ID_fixedbv ||
267  src.id()==ID_c_bool ||
268  src.id()==ID_bool ||
269  src.id()==ID_c_enum_tag ||
270  src.id()==ID_c_bit_field ||
271  src.id()==ID_integer ||
272  src.id()==ID_real;
273  }
274 
275  typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
277 
278  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
279 };
280 
282 {
283 public:
285  : expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
286  {
287  }
288 
289  static void make_already_typechecked(exprt &expr)
290  {
292  expr.swap(a);
293  }
294 
296  {
297  return op0();
298  }
299 };
300 
302 {
303 public:
305  : type_with_subtypet(ID_already_typechecked, std::move(type))
306  {
307  }
308 
309  static void make_already_typechecked(typet &type)
310  {
312  type.swap(a);
313  }
314 
316  {
317  return subtype();
318  }
319 };
320 
322 {
323  PRECONDITION(expr.id() == ID_already_typechecked);
324  PRECONDITION(expr.operands().size() == 1);
325 
326  return static_cast<already_typechecked_exprt &>(expr);
327 }
328 
330 {
331  PRECONDITION(type.id() == ID_already_typechecked);
332  PRECONDITION(type.has_subtype());
333 
334  return static_cast<already_typechecked_typet &>(type);
335 }
336 
337 #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_assigns_exprs
virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:858
c_typecheck_baset::typecheck_expr_side_effect
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:1768
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:170
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:1439
ansi_c_declaration.h
ANSI-CC Language Type Checking.
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:3042
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:896
c_typecheck_baset::typecheck_expr_builtin_offsetof
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
Definition: c_typecheck_expr.cpp:552
c_typecheck_baset::typecheck_expr_shifts
virtual void typecheck_expr_shifts(shift_exprt &expr)
Definition: c_typecheck_expr.cpp:3183
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:1669
c_typecheck_baset::do_special_functions
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
Definition: c_typecheck_expr.cpp:2037
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:321
c_typecheck_baset::enum_constant_type
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
Definition: c_typecheck_type.cpp:1056
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:1281
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:2117
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
c_typecheck_baset::add_rounding_mode
static void add_rounding_mode(exprt &)
Definition: c_typecheck_expr.cpp:56
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:2914
already_typechecked_typet
Definition: c_typecheck_base.h:302
c_typecheck_baset::typecheck_side_effect_statement_expression
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
Definition: c_typecheck_expr.cpp:888
c_typecheck_baset::typecheck_expr_symbol
virtual void typecheck_expr_symbol(exprt &expr)
Definition: c_typecheck_expr.cpp:785
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:1088
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:3275
c_typecheck_baset::asm_label_mapt
std::unordered_map< irep_idt, irep_idt > asm_label_mapt
Definition: c_typecheck_base.h:275
c_typecheck_baset::typecheck_expr_rel_vector
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
Definition: c_typecheck_expr.cpp:1395
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:1652
c_typecheck_baset::typecheck_expr_alignof
virtual void typecheck_expr_alignof(exprt &expr)
Definition: c_typecheck_expr.cpp:1013
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:1513
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:1856
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:1456
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:3070
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:3362
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
c_typecheck_baset::clean_code
std::list< codet > clean_code
Definition: c_typecheck_base.h:242
to_already_typechecked_type
already_typechecked_typet & to_already_typechecked_type(typet &type)
Definition: c_typecheck_base.h:329
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:3552
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:866
c_typecheck_baset::typecheck_expr_operands
virtual void typecheck_expr_operands(exprt &expr)
Definition: c_typecheck_expr.cpp:711
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:1454
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:284
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:276
expr_protectedt::op0
exprt & op0()
Definition: expr.h:102
c_typecheck_baset::typecheck_assigns
virtual void typecheck_assigns(const code_typet &function_declarator, const irept &spec)
Definition: c_typecheck_code.cpp:808
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:958
c_typecheck_baset::typecheck_expr_rel
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
Definition: c_typecheck_expr.cpp:1293
messaget::result
mstreamt & result() const
Definition: message.h:409
ansi_c_declaratort
Definition: ansi_c_declaration.h:21
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:3000
already_typechecked_exprt::make_already_typechecked
static void make_already_typechecked(exprt &expr)
Definition: c_typecheck_base.h:289
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:1757
already_typechecked_exprt::get_expr
exprt & get_expr()
Definition: c_typecheck_base.h:295
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:1721
typecheck.h
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1127
c_typecheck_baset::move_symbol
void move_symbol(symbolt &symbol)
Definition: c_typecheck_base.h:246
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1375
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:155
c_typecheck_baset::continue_is_allowed
bool continue_is_allowed
Definition: c_typecheck_base.h:154
c_typecheck_baset::is_complete_type
virtual bool is_complete_type(const typet &type) const
Definition: c_typecheck_code.cpp:342
std_types.h
Pre-defined types.
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:1392
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:3030
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:91
already_typechecked_typet::already_typechecked_typet
already_typechecked_typet(typet type)
Definition: c_typecheck_base.h:304
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:1624
c_typecheck_baset::typecheck_arithmetic_pointer
virtual void typecheck_arithmetic_pointer(const exprt &expr)
Definition: c_typecheck_expr.cpp:3250
code_typet
Base type of functions.
Definition: std_types.h:736
c_typecheck_baset::make_constant_index
virtual void make_constant_index(exprt &expr)
Definition: c_typecheck_expr.cpp:3573
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
c_typecheck_baset::typecheck_expr_trinary
virtual void typecheck_expr_trinary(if_exprt &expr)
Definition: c_typecheck_expr.cpp:1533
c_typecheck_baset::typecheck_typedef_type
virtual void typecheck_typedef_type(typet &type)
Definition: c_typecheck_type.cpp:1572
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:1536
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:3376
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:315
c_typecheck_baset::labels_used
std::map< irep_idt, source_locationt > labels_used
Definition: c_typecheck_base.h:160
c_typecheck_baset::typecheck_expr_ptrmember
virtual void typecheck_expr_ptrmember(exprt &expr)
Definition: c_typecheck_expr.cpp:1420
c_typecheck_baset::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: c_typecheck_expr.cpp:41
c_typecheck_baset::switch_op_type
typet switch_op_type
Definition: c_typecheck_base.h:156
source_locationt
Definition: source_location.h:20
c_typecheck_baset::break_is_allowed
bool break_is_allowed
Definition: c_typecheck_base.h:153
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:2496
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:260
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:1310
c_typecheck_baset::typecheck_expr_main
virtual void typecheck_expr_main(exprt &expr)
Definition: c_typecheck_expr.cpp:168
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:718
c_typecheck_baset::labels_defined
std::map< irep_idt, source_locationt > labels_defined
Definition: c_typecheck_base.h:160
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:535
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:157
c_typecheck_baset::typecheck_expr_constant
virtual void typecheck_expr_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:2995
c_typecheck_baset::~c_typecheck_baset
virtual ~c_typecheck_baset()
Definition: c_typecheck_base.h:61
already_typechecked_exprt
Definition: c_typecheck_base.h:282
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:309
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:574
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
c_typecheck_baset::typecheck_c_enum_type
virtual void typecheck_c_enum_type(typet &type)
Definition: c_typecheck_type.cpp:1146
c_typecheck_baset::increment_designator
void increment_designator(designatort &designator)
Definition: c_typecheck_initializer.cpp:664
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
ANSI-C Language Type Checking.
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:920
std_expr.h
API to expression classes.
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:1866
c_typecheck_baset::typecheck_compound_body
virtual void typecheck_compound_body(struct_union_typet &type)
Definition: c_typecheck_type.cpp:880
c_typecheck_baset::typecheck_expr_index
virtual void typecheck_expr_index(exprt &expr)
Definition: c_typecheck_expr.cpp:1223
expr_protectedt
Base class for all expressions.
Definition: expr.h:367
c_typecheck_baset::make_index_type
virtual void make_index_type(exprt &expr)
Definition: c_typecheck_expr.cpp:1218
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:494
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:1621
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:485
c_typecheck_baset::typecheck_expr_typecast
virtual void typecheck_expr_typecast(exprt &expr)
Definition: c_typecheck_expr.cpp:1035