cprover
c_typecheck_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_typecheck_base.h"
13 
14 #include <util/config.h>
15 #include <util/expr_initializer.h>
16 
17 #include "ansi_c_declaration.h"
18 
20 {
22 }
23 
25 {
26  if(code.id()!=ID_code)
27  {
29  error() << "expected code, got " << code.pretty() << eom;
30  throw 0;
31  }
32 
33  code.type()=code_typet();
34 
35  const irep_idt &statement=code.get_statement();
36 
37  if(statement==ID_expression)
39  else if(statement==ID_label)
41  else if(statement==ID_switch_case)
43  else if(statement==ID_gcc_switch_case_range)
45  else if(statement==ID_block)
47  else if(statement==ID_decl_block)
48  {
49  }
50  else if(statement==ID_ifthenelse)
52  else if(statement==ID_while)
54  else if(statement==ID_dowhile)
56  else if(statement==ID_for)
57  typecheck_for(code);
58  else if(statement==ID_switch)
60  else if(statement==ID_break)
61  typecheck_break(code);
62  else if(statement==ID_goto)
64  else if(statement==ID_gcc_computed_goto)
66  else if(statement==ID_continue)
67  typecheck_continue(code);
68  else if(statement==ID_return)
69  typecheck_return(code);
70  else if(statement==ID_decl)
71  typecheck_decl(code);
72  else if(statement==ID_assign)
73  typecheck_assign(code);
74  else if(statement==ID_skip)
75  {
76  }
77  else if(statement==ID_asm)
78  typecheck_asm(code);
79  else if(statement==ID_start_thread)
81  else if(statement==ID_gcc_local_label)
83  else if(statement==ID_msc_try_finally)
84  {
85  assert(code.operands().size()==2);
86  typecheck_code(to_code(code.op0()));
87  typecheck_code(to_code(code.op1()));
88  }
89  else if(statement==ID_msc_try_except)
90  {
91  assert(code.operands().size()==3);
92  typecheck_code(to_code(code.op0()));
93  typecheck_expr(code.op1());
94  typecheck_code(to_code(code.op2()));
95  }
96  else if(statement==ID_msc_leave)
97  {
98  // fine as is, but should check that we
99  // are in a 'try' block
100  }
101  else if(statement==ID_static_assert)
102  {
103  assert(code.operands().size()==2);
104  typecheck_expr(code.op0());
105  typecheck_expr(code.op1());
106  }
107  else if(statement==ID_CPROVER_try_catch ||
108  statement==ID_CPROVER_try_finally)
109  {
110  assert(code.operands().size()==2);
111  typecheck_code(to_code(code.op0()));
112  typecheck_code(to_code(code.op1()));
113  }
114  else if(statement==ID_CPROVER_throw)
115  {
116  assert(code.operands().empty());
117  }
118  else if(statement==ID_assume ||
119  statement==ID_assert)
120  {
121  // These are not generated by the C/C++ parsers,
122  // but we allow them for the benefit of other users
123  // of the typechecker.
124  assert(code.operands().size()==1);
125  typecheck_expr(code.op0());
126  }
127  else
128  {
130  error() << "unexpected statement: " << statement << eom;
131  throw 0;
132  }
133 }
134 
136 {
137  const irep_idt flavor=to_code_asm(code).get_flavor();
138 
139  if(flavor==ID_gcc)
140  {
141  // These have 5 operands.
142  // The first parameter is a string.
143  // Parameters 1, 2, 3, 4 are lists of expressions.
144 
145  // Parameter 1: OutputOperands
146  // Parameter 2: InputOperands
147  // Parameter 3: Clobbers
148  // Parameter 4: GotoLabels
149 
150  assert(code.operands().size()==5);
151 
152  typecheck_expr(code.op0());
153 
154  for(std::size_t i=1; i<code.operands().size(); i++)
155  {
156  exprt &list=code.operands()[i];
157  Forall_operands(it, list)
158  typecheck_expr(*it);
159  }
160  }
161  else if(flavor==ID_msc)
162  {
163  assert(code.operands().size()==1);
164  typecheck_expr(code.op0());
165  }
166 }
167 
169 {
170  if(code.operands().size()!=2)
171  {
173  error() << "assignment statement expected to have two operands"
174  << eom;
175  throw 0;
176  }
177 
178  typecheck_expr(code.op0());
179  typecheck_expr(code.op1());
180 
181  implicit_typecast(code.op1(), code.op0().type());
182 }
183 
185 {
186  for(auto &c : code.statements())
187  typecheck_code(c);
188 
189  // do decl-blocks
190 
191  code_blockt new_ops;
192  new_ops.statements().reserve(code.statements().size());
193 
194  for(auto &code_op : code.statements())
195  {
196  if(code_op.is_not_nil())
197  new_ops.add(std::move(code_op));
198  }
199 
200  code.statements().swap(new_ops.statements());
201 }
202 
204 {
205  if(!break_is_allowed)
206  {
208  error() << "break not allowed here" << eom;
209  throw 0;
210  }
211 }
212 
214 {
216  {
218  error() << "continue not allowed here" << eom;
219  throw 0;
220  }
221 }
222 
224 {
225  // this comes with 1 operand, which is a declaration
226  if(code.operands().size()!=1)
227  {
229  error() << "decl expected to have 1 operand" << eom;
230  throw 0;
231  }
232 
233  // op0 must be declaration
234  if(code.op0().id()!=ID_declaration)
235  {
237  error() << "decl statement expected to have declaration as operand"
238  << eom;
239  throw 0;
240  }
241 
242  ansi_c_declarationt declaration;
243  declaration.swap(code.op0());
244 
245  if(declaration.get_is_static_assert())
246  {
247  assert(declaration.operands().size()==2);
248  codet new_code(ID_static_assert);
249  new_code.add_source_location()=code.source_location();
250  new_code.operands().swap(declaration.operands());
251  code.swap(new_code);
252  typecheck_code(code);
253  return; // done
254  }
255 
256  typecheck_declaration(declaration);
257 
258  std::list<codet> new_code;
259 
260  // iterate over declarators
261 
262  for(ansi_c_declarationt::declaratorst::const_iterator
263  d_it=declaration.declarators().begin();
264  d_it!=declaration.declarators().end();
265  d_it++)
266  {
267  irep_idt identifier=d_it->get_name();
268 
269  // look it up
270  symbol_tablet::symbolst::const_iterator s_it=
271  symbol_table.symbols.find(identifier);
272 
273  if(s_it==symbol_table.symbols.end())
274  {
276  error() << "failed to find decl symbol `" << identifier
277  << "' in symbol table" << eom;
278  throw 0;
279  }
280 
281  const symbolt &symbol=s_it->second;
282 
283  // This must not be an incomplete type, unless it's 'extern'
284  // or a typedef.
285  if(!symbol.is_type &&
286  !symbol.is_extern &&
287  !is_complete_type(symbol.type))
288  {
289  error().source_location=symbol.location;
290  error() << "incomplete type not permitted here" << eom;
291  throw 0;
292  }
293 
294  // see if it's a typedef
295  // or a function
296  // or static
297  if(symbol.is_type ||
298  symbol.type.id()==ID_code ||
299  symbol.is_static_lifetime)
300  {
301  // we ignore
302  }
303  else
304  {
305  code_declt decl(symbol.symbol_expr());
306  decl.add_source_location() = symbol.location;
307  decl.symbol().add_source_location() = symbol.location;
308 
309  // add initializer, if any
310  if(symbol.value.is_not_nil())
311  {
312  decl.operands().resize(2);
313  decl.op1() = symbol.value;
314  }
315 
316  new_code.push_back(decl);
317  }
318  }
319 
320  // stash away any side-effects in the declaration
321  new_code.splice(new_code.begin(), clean_code);
322 
323  if(new_code.empty())
324  {
325  source_locationt source_location=code.source_location();
326  code=code_skipt();
327  code.add_source_location()=source_location;
328  }
329  else if(new_code.size()==1)
330  {
331  code.swap(new_code.front());
332  }
333  else
334  {
335  // build a decl-block
336  auto code_block=code_blockt::from_list(new_code);
337  code_block.set_statement(ID_decl_block);
338  code.swap(code_block);
339  }
340 }
341 
343 {
344  if(type.id()==ID_incomplete_struct ||
345  type.id()==ID_incomplete_union)
346  return false;
347  else if(type.id()==ID_array)
348  {
349  if(to_array_type(type).size().is_nil())
350  return false;
351  return is_complete_type(type.subtype());
352  }
353  else if(type.id()==ID_struct || type.id()==ID_union)
354  {
355  for(const auto &c : to_struct_union_type(type).components())
356  if(!is_complete_type(c.type()))
357  return false;
358  }
359  else if(type.id()==ID_vector)
360  return is_complete_type(type.subtype());
361  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
362  {
363  return is_complete_type(follow(type));
364  }
365 
366  return true;
367 }
368 
370 {
371  if(code.operands().size()!=1)
372  {
374  error() << "expression statement expected to have one operand"
375  << eom;
376  throw 0;
377  }
378 
379  exprt &op=code.op0();
380  typecheck_expr(op);
381 }
382 
384 {
385  if(code.operands().size()!=4)
386  {
388  error() << "for expected to have four operands" << eom;
389  throw 0;
390  }
391 
392  // the "for" statement has an implicit block around it,
393  // since code.op0() may contain declarations
394  //
395  // we therefore transform
396  //
397  // for(a;b;c) d;
398  //
399  // to
400  //
401  // { a; for(;b;c) d; }
402  //
403  // if config.ansi_c.for_has_scope
404 
406  code.op0().is_nil())
407  {
408  if(code.op0().is_not_nil())
409  typecheck_code(to_code(code.op0()));
410 
411  if(code.op1().is_nil())
412  code.op1()=true_exprt();
413  else
414  {
415  typecheck_expr(code.op1());
416  implicit_typecast_bool(code.op1());
417  }
418 
419  if(code.op2().is_not_nil())
420  typecheck_expr(code.op2());
421 
422  if(code.op3().is_not_nil())
423  {
424  // save & set flags
425  bool old_break_is_allowed=break_is_allowed;
426  bool old_continue_is_allowed=continue_is_allowed;
427 
429 
430  // recursive call
431  if(to_code(code.op3()).get_statement()==ID_decl_block)
432  {
433  code_blockt code_block;
434  code_block.add_source_location()=code.op3().source_location();
435 
436  code_block.add(std::move(to_code(code.op3())));
437  code.op3().swap(code_block);
438  }
439  typecheck_code(to_code(code.op3()));
440 
441  // restore flags
442  break_is_allowed=old_break_is_allowed;
443  continue_is_allowed=old_continue_is_allowed;
444  }
445  }
446  else
447  {
448  code_blockt code_block;
449  code_block.add_source_location()=code.source_location();
450  if(to_code(code.op3()).get_statement()==ID_block)
451  {
452  code_block.set(
453  ID_C_end_location,
455  }
456  else
457  {
458  code_block.set(
459  ID_C_end_location,
460  code.op3().source_location());
461  }
462 
463  code_block.reserve_operands(2);
464  code_block.add(std::move(to_code(code.op0())));
465  code.op0().make_nil();
466  code_block.add(std::move(code));
467  code.swap(code_block);
468  typecheck_code(code); // recursive call
469  }
470 
471  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
472 }
473 
475 {
476  // record the label
478 
479  typecheck_code(code.code());
480 }
481 
483 {
484  if(code.operands().size()!=2)
485  {
487  error() << "switch_case expected to have two operands" << eom;
488  throw 0;
489  }
490 
491  typecheck_code(code.code());
492 
493  if(code.is_default())
494  {
495  if(!case_is_allowed)
496  {
498  error() << "did not expect default label here" << eom;
499  throw 0;
500  }
501  }
502  else
503  {
504  if(!case_is_allowed)
505  {
507  error() << "did not expect `case' here" << eom;
508  throw 0;
509  }
510 
511  exprt &case_expr=code.case_op();
512  typecheck_expr(case_expr);
513  implicit_typecast(case_expr, switch_op_type);
514  make_constant(case_expr);
515  }
516 }
517 
519 {
520  if(code.operands().size()!=3)
521  {
523  error() << "gcc_switch_case_range expected to have three operands"
524  << eom;
525  throw 0;
526  }
527 
528  typecheck_code(to_code(code.op2()));
529 
530  if(!case_is_allowed)
531  {
533  error() << "did not expect `case' here" << eom;
534  throw 0;
535  }
536 
537  typecheck_expr(code.op0());
538  typecheck_expr(code.op1());
541  make_constant(code.op0());
542  make_constant(code.op1());
543 }
544 
546 {
547  // these are just declarations, e.g.,
548  // __label__ here, there;
549 }
550 
552 {
553  // we record the label used
555 }
556 
558 {
559  if(code.operands().size()!=1)
560  {
562  error() << "computed-goto expected to have one operand" << eom;
563  throw 0;
564  }
565 
566  exprt &dest=code.op0();
567 
568  if(dest.id()!=ID_dereference)
569  {
571  error() << "computed-goto expected to have dereferencing operand"
572  << eom;
573  throw 0;
574  }
575 
576  assert(dest.operands().size()==1);
577 
578  typecheck_expr(dest.op0());
579  dest.type()=empty_typet();
580 }
581 
583 {
584  if(code.operands().size()!=3)
585  {
587  error() << "ifthenelse expected to have three operands" << eom;
588  throw 0;
589  }
590 
591  exprt &cond=code.cond();
592 
593  typecheck_expr(cond);
594 
595  #if 0
596  if(cond.id()==ID_sideeffect &&
597  cond.get(ID_statement)==ID_assign)
598  {
599  warning("warning: assignment in if condition");
600  }
601  #endif
602 
604 
605  if(code.then_case().get_statement() == ID_decl_block)
606  {
607  code_blockt code_block({code.then_case()});
608  code_block.add_source_location()=code.then_case().source_location();
609  code.then_case() = code_block;
610  }
611 
612  typecheck_code(code.then_case());
613 
614  if(!code.else_case().is_nil())
615  {
616  if(code.else_case().get_statement() == ID_decl_block)
617  {
618  code_blockt code_block({code.else_case()});
619  code_block.add_source_location()=code.else_case().source_location();
620  code.else_case() = code_block;
621  }
622 
623  typecheck_code(code.else_case());
624  }
625 }
626 
628 {
629  if(code.operands().size()!=1)
630  {
632  error() << "start_thread expected to have one operand" << eom;
633  throw 0;
634  }
635 
636  typecheck_code(to_code(code.op0()));
637 }
638 
640 {
641  if(code.operands().empty())
642  {
643  if(follow(return_type).id()!=ID_empty &&
644  return_type.id()!=ID_constructor &&
645  return_type.id()!=ID_destructor)
646  {
647  // gcc doesn't actually complain, it just warns!
649  warning() << "non-void function should return a value" << eom;
650 
651  code.copy_to_operands(
653  }
654  }
655  else if(code.operands().size()==1)
656  {
657  typecheck_expr(code.op0());
658 
659  if(follow(return_type).id()==ID_empty)
660  {
661  // gcc doesn't actually complain, it just warns!
662  if(follow(code.op0().type()).id()!=ID_empty)
663  {
665 
666  warning() << "function has return void ";
667  warning() << "but a return statement returning ";
668  warning() << to_string(follow(code.op0().type()));
669  warning() << eom;
670 
671  code.op0().make_typecast(return_type);
672  }
673  }
674  else
676  }
677  else
678  {
680  error() << "return expected to have 0 or 1 operands" << eom;
681  throw 0;
682  }
683 }
684 
686 {
687  if(code.operands().size()!=2)
688  {
690  error() << "switch expects two operands" << eom;
691  throw 0;
692  }
693 
694  typecheck_expr(code.value());
695 
696  // this needs to be promoted
698 
699  // save & set flags
700 
701  bool old_case_is_allowed(case_is_allowed);
702  bool old_break_is_allowed(break_is_allowed);
703  typet old_switch_op_type(switch_op_type);
704 
705  switch_op_type=code.value().type();
707 
708  typecheck_code(code.body());
709 
710  // restore flags
711  case_is_allowed=old_case_is_allowed;
712  break_is_allowed=old_break_is_allowed;
713  switch_op_type=old_switch_op_type;
714 }
715 
717 {
718  if(code.operands().size()!=2)
719  {
721  error() << "while expected to have two operands" << eom;
722  throw 0;
723  }
724 
725  typecheck_expr(code.cond());
727 
728  // save & set flags
729  bool old_break_is_allowed(break_is_allowed);
730  bool old_continue_is_allowed(continue_is_allowed);
731 
733 
734  if(code.body().get_statement()==ID_decl_block)
735  {
736  code_blockt code_block({code.body()});
737  code_block.add_source_location()=code.body().source_location();
738  code.body() = code_block;
739  }
740  typecheck_code(code.body());
741 
742  // restore flags
743  break_is_allowed=old_break_is_allowed;
744  continue_is_allowed=old_continue_is_allowed;
745 
746  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
747 }
748 
750 {
751  if(code.operands().size()!=2)
752  {
754  error() << "do while expected to have two operands" << eom;
755  throw 0;
756  }
757 
758  typecheck_expr(code.cond());
760 
761  // save & set flags
762  bool old_break_is_allowed(break_is_allowed);
763  bool old_continue_is_allowed(continue_is_allowed);
764 
766 
767  if(code.body().get_statement()==ID_decl_block)
768  {
769  code_blockt code_block({code.body()});
770  code_block.add_source_location()=code.body().source_location();
771  code.body() = code_block;
772  }
773  typecheck_code(code.body());
774 
775  // restore flags
776  break_is_allowed=old_break_is_allowed;
777  continue_is_allowed=old_continue_is_allowed;
778 
779  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
780 }
781 
783  codet &code,
784  const irep_idt &spec)
785 {
786  if(code.find(spec).is_not_nil())
787  {
788  exprt &constraint=
789  static_cast<exprt&>(code.add(spec));
790 
791  typecheck_expr(constraint);
792  implicit_typecast_bool(constraint);
793  }
794 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
exprt::op2
exprt & op2()
Definition: expr.h:90
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
code_switch_caset::case_op
const exprt & case_op() const
Definition: std_code.h:1351
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
c_typecheck_baset::typecheck_asm
virtual void typecheck_asm(codet &code)
Definition: c_typecheck_code.cpp:135
typet::subtype
const typet & subtype() const
Definition: type.h:38
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1326
exprt::op3
exprt & op3()
Definition: expr.h:93
ansi_c_declaration.h
code_blockt::from_list
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:169
ansi_c_declarationt::declarators
const declaratorst & declarators() const
Definition: ansi_c_declaration.h:217
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
code_whilet
codet representing a while statement.
Definition: std_code.h:767
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:44
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
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
irept::make_nil
void make_nil()
Definition: irep.h:315
typet
The type of an expression, extends irept.
Definition: type.h:27
c_typecheck_base.h
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:652
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
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
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
c_typecheck_baset::typecheck_return
virtual void typecheck_return(codet &code)
Definition: c_typecheck_code.cpp:639
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
to_code_while
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:814
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:642
messaget::eom
static eomt eom
Definition: message.h:284
c_typecheck_baset::typecheck_spec_expr
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:782
configt::ansi_c
struct configt::ansi_ct ansi_c
ansi_c_declarationt::get_is_static_assert
bool get_is_static_assert() const
Definition: ansi_c_declaration.h:179
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:614
code_labelt::code
codet & code()
Definition: std_code.h:1289
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
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
to_code_switch_case
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1382
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:159
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
c_typecheck_baset::typecheck_continue
virtual void typecheck_continue(codet &code)
Definition: c_typecheck_code.cpp:213
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:829
expr_initializer.h
messaget::error
mstreamt & error() const
Definition: message.h:386
empty_typet
The empty type.
Definition: std_types.h:48
code_switch_caset::is_default
bool is_default() const
Definition: std_code.h:1341
c_typecheck_baset::implicit_typecast_bool
virtual void implicit_typecast_bool(exprt &expr)
Definition: c_typecheck_base.h:117
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
to_code_goto
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1017
c_typecheck_baset::typecheck_label
virtual void typecheck_label(code_labelt &code)
Definition: c_typecheck_code.cpp:474
code_gotot
codet representation of a goto statement.
Definition: std_code.h:983
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:688
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1256
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
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1310
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
c_typecheck_baset::typecheck_expression
virtual void typecheck_expression(codet &code)
Definition: c_typecheck_code.cpp:369
exprt::op1
exprt & op1()
Definition: expr.h:87
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:67
to_code_dowhile
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:876
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
irept::swap
void swap(irept &irep)
Definition: irep.h:303
code_typet
Base type of functions.
Definition: std_types.h:751
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:783
code_whilet::body
const codet & body() const
Definition: std_code.h:793
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
code_blockt::add
void add(const codet &code)
Definition: std_code.h:189
c_typecheck_baset::typecheck_dowhile
virtual void typecheck_dowhile(code_dowhilet &code)
Definition: c_typecheck_code.cpp:749
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:360
c_typecheck_baset::labels_used
std::map< irep_idt, source_locationt > labels_used
Definition: c_typecheck_base.h:155
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
config
configt config
Definition: config.cpp:24
c_typecheck_baset::switch_op_type
typet switch_op_type
Definition: c_typecheck_base.h:151
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
c_typecheck_baset::break_is_allowed
bool break_is_allowed
Definition: c_typecheck_base.h:148
code_labelt::get_label
const irep_idt & get_label() const
Definition: std_code.h:1279
to_code_asm
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1490
c_typecheck_baset::typecheck_for
virtual void typecheck_for(codet &code)
Definition: c_typecheck_code.cpp:383
code_switcht::value
const exprt & value() const
Definition: std_code.h:721
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
ansi_c_declarationt
Definition: ansi_c_declaration.h:72
c_typecheck_baset::typecheck_decl
virtual void typecheck_decl(codet &code)
Definition: c_typecheck_code.cpp:223
code_skipt
A codet representing a skip statement.
Definition: std_code.h:237
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
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
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
code_dowhilet::body
const codet & body() const
Definition: std_code.h:855
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
code_ifthenelset::else_case
const codet & else_case() const
Definition: std_code.h:662
c_typecheck_baset::typecheck_assign
virtual void typecheck_assign(codet &expr)
Definition: c_typecheck_code.cpp:168
to_code_switch
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:752
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:152
code_gotot::get_destination
const irep_idt & get_destination() const
Definition: std_code.h:1001
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
code_switch_caset::code
codet & code()
Definition: std_code.h:1361
c_typecheck_baset::typecheck_start_thread
virtual void typecheck_start_thread(codet &code)
Definition: c_typecheck_code.cpp:627
config.h
code_dowhilet::cond
const exprt & cond() const
Definition: std_code.h:845
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:582
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
exprt::operands
operandst & operands()
Definition: expr.h:78
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_gcc_computed_goto
virtual void typecheck_gcc_computed_goto(codet &code)
Definition: c_typecheck_code.cpp:557
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
code_asmt::get_flavor
const irep_idt & get_flavor() const
Definition: std_code.h:1471
code_switcht::body
const codet & body() const
Definition: std_code.h:731
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:56
messaget::warning
mstreamt & warning() const
Definition: message.h:391
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
c_typecheck_baset::typecheck_gcc_local_label
virtual void typecheck_gcc_local_label(codet &code)
Definition: c_typecheck_code.cpp:545
code_blockt::end_location
source_locationt end_location() const
Definition: std_code.h:208
c_typecheck_baset::typecheck_block
virtual void typecheck_block(code_blockt &code)
Definition: c_typecheck_code.cpp:184
c_typecheck_baset::implicit_typecast
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecheck_typecast.cpp:13
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34