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  {
28  err_location(code);
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)
46  typecheck_block(code);
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  {
129  err_location(code);
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  {
172  err_location(code);
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  Forall_operands(it, code)
187  typecheck_code(to_code(*it));
188 
189  // do decl-blocks
190 
191  exprt new_ops;
192  new_ops.operands().reserve(code.operands().size());
193 
194  Forall_operands(it1, code)
195  {
196  if(it1->is_nil())
197  continue;
198 
199  codet &code_op=to_code(*it1);
200 
201  if(code_op.get_statement()==ID_label)
202  {
203  // these may be nested
204  codet *code_ptr=&code_op;
205 
206  while(code_ptr->get_statement()==ID_label)
207  {
208  assert(code_ptr->operands().size()==1);
209  code_ptr=&to_code(code_ptr->op0());
210  }
211 
212  // codet &label_op=*code_ptr;
213 
214  new_ops.move_to_operands(code_op);
215  }
216  else
217  new_ops.move_to_operands(code_op);
218  }
219 
220  code.operands().swap(new_ops.operands());
221 }
222 
224 {
225  if(!break_is_allowed)
226  {
227  err_location(code);
228  error() << "break not allowed here" << eom;
229  throw 0;
230  }
231 }
232 
234 {
236  {
237  err_location(code);
238  error() << "continue not allowed here" << eom;
239  throw 0;
240  }
241 }
242 
244 {
245  // this comes with 1 operand, which is a declaration
246  if(code.operands().size()!=1)
247  {
248  err_location(code);
249  error() << "decl expected to have 1 operand" << eom;
250  throw 0;
251  }
252 
253  // op0 must be declaration
254  if(code.op0().id()!=ID_declaration)
255  {
256  err_location(code);
257  error() << "decl statement expected to have declaration as operand"
258  << eom;
259  throw 0;
260  }
261 
262  ansi_c_declarationt declaration;
263  declaration.swap(code.op0());
264 
265  if(declaration.get_is_static_assert())
266  {
267  assert(declaration.operands().size()==2);
268  codet new_code(ID_static_assert);
269  new_code.add_source_location()=code.source_location();
270  new_code.operands().swap(declaration.operands());
271  code.swap(new_code);
272  typecheck_code(code);
273  return; // done
274  }
275 
276  typecheck_declaration(declaration);
277 
278  std::list<codet> new_code;
279 
280  // iterate over declarators
281 
282  for(ansi_c_declarationt::declaratorst::const_iterator
283  d_it=declaration.declarators().begin();
284  d_it!=declaration.declarators().end();
285  d_it++)
286  {
287  irep_idt identifier=d_it->get_name();
288 
289  // look it up
290  symbol_tablet::symbolst::const_iterator s_it=
291  symbol_table.symbols.find(identifier);
292 
293  if(s_it==symbol_table.symbols.end())
294  {
295  err_location(code);
296  error() << "failed to find decl symbol `" << identifier
297  << "' in symbol table" << eom;
298  throw 0;
299  }
300 
301  const symbolt &symbol=s_it->second;
302 
303  // This must not be an incomplete type, unless it's 'extern'
304  // or a typedef.
305  if(!symbol.is_type &&
306  !symbol.is_extern &&
307  !is_complete_type(symbol.type))
308  {
309  error().source_location=symbol.location;
310  error() << "incomplete type not permitted here" << eom;
311  throw 0;
312  }
313 
314  // see if it's a typedef
315  // or a function
316  // or static
317  if(symbol.is_type ||
318  symbol.type.id()==ID_code ||
319  symbol.is_static_lifetime)
320  {
321  // we ignore
322  }
323  else
324  {
325  code_declt code;
326  code.add_source_location()=symbol.location;
327  code.symbol()=symbol.symbol_expr();
328  code.symbol().add_source_location()=symbol.location;
329 
330  // add initializer, if any
331  if(symbol.value.is_not_nil())
332  {
333  code.operands().resize(2);
334  code.op1()=symbol.value;
335  }
336 
337  new_code.push_back(code);
338  }
339  }
340 
341  // stash away any side-effects in the declaration
342  new_code.splice(new_code.begin(), clean_code);
343 
344  if(new_code.empty())
345  {
346  source_locationt source_location=code.source_location();
347  code=code_skipt();
348  code.add_source_location()=source_location;
349  }
350  else if(new_code.size()==1)
351  {
352  code.swap(new_code.front());
353  }
354  else
355  {
356  // build a decl-block
357  code_blockt code_block(new_code);
358  code_block.set_statement(ID_decl_block);
359  code.swap(code_block);
360  }
361 }
362 
364 {
365  if(type.id()==ID_incomplete_struct ||
366  type.id()==ID_incomplete_union)
367  return false;
368  else if(type.id()==ID_array)
369  {
370  if(to_array_type(type).size().is_nil())
371  return false;
372  return is_complete_type(type.subtype());
373  }
374  else if(type.id()==ID_struct || type.id()==ID_union)
375  {
376  const struct_union_typet::componentst &components=
378  for(struct_union_typet::componentst::const_iterator
379  it=components.begin();
380  it!=components.end();
381  it++)
382  if(!is_complete_type(it->type()))
383  return false;
384  }
385  else if(type.id()==ID_vector)
386  return is_complete_type(type.subtype());
387  else if(type.id()==ID_symbol)
388  return is_complete_type(follow(type));
389 
390  return true;
391 }
392 
394 {
395  if(code.operands().size()!=1)
396  {
397  err_location(code);
398  error() << "expression statement expected to have one operand"
399  << eom;
400  throw 0;
401  }
402 
403  exprt &op=code.op0();
404  typecheck_expr(op);
405 }
406 
408 {
409  if(code.operands().size()!=4)
410  {
411  err_location(code);
412  error() << "for expected to have four operands" << eom;
413  throw 0;
414  }
415 
416  // the "for" statement has an implicit block around it,
417  // since code.op0() may contain declarations
418  //
419  // we therefore transform
420  //
421  // for(a;b;c) d;
422  //
423  // to
424  //
425  // { a; for(;b;c) d; }
426  //
427  // if config.ansi_c.for_has_scope
428 
430  code.op0().is_nil())
431  {
432  if(code.op0().is_not_nil())
433  typecheck_code(to_code(code.op0()));
434 
435  if(code.op1().is_nil())
436  code.op1()=true_exprt();
437  else
438  {
439  typecheck_expr(code.op1());
440  implicit_typecast_bool(code.op1());
441  }
442 
443  if(code.op2().is_not_nil())
444  typecheck_expr(code.op2());
445 
446  if(code.op3().is_not_nil())
447  {
448  // save & set flags
449  bool old_break_is_allowed=break_is_allowed;
450  bool old_continue_is_allowed=continue_is_allowed;
451 
453 
454  // recursive call
455  if(to_code(code.op3()).get_statement()==ID_decl_block)
456  {
457  code_blockt code_block;
458  code_block.add_source_location()=code.op3().source_location();
459 
460  code_block.move_to_operands(code.op3());
461  code.op3().swap(code_block);
462  }
463  typecheck_code(to_code(code.op3()));
464 
465  // restore flags
466  break_is_allowed=old_break_is_allowed;
467  continue_is_allowed=old_continue_is_allowed;
468  }
469  }
470  else
471  {
472  code_blockt code_block;
473  code_block.add_source_location()=code.source_location();
474  if(to_code(code.op3()).get_statement()==ID_block)
475  {
476  code_block.set(
477  ID_C_end_location,
479  }
480  else
481  {
482  code_block.set(
483  ID_C_end_location,
484  code.op3().source_location());
485  }
486 
487  code_block.reserve_operands(2);
488  code_block.move_to_operands(code.op0());
489  code.op0().make_nil();
490  code_block.move_to_operands(code);
491  code.swap(code_block);
492  typecheck_code(code); // recursive call
493  }
494 
495  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
496 }
497 
499 {
500  // record the label
502 
503  typecheck_code(code.code());
504 }
505 
507 {
508  if(code.operands().size()!=2)
509  {
510  err_location(code);
511  error() << "switch_case expected to have two operands" << eom;
512  throw 0;
513  }
514 
515  typecheck_code(code.code());
516 
517  if(code.is_default())
518  {
519  if(!case_is_allowed)
520  {
521  err_location(code);
522  error() << "did not expect default label here" << eom;
523  throw 0;
524  }
525  }
526  else
527  {
528  if(!case_is_allowed)
529  {
530  err_location(code);
531  error() << "did not expect `case' here" << eom;
532  throw 0;
533  }
534 
535  exprt &case_expr=code.case_op();
536  typecheck_expr(case_expr);
537  implicit_typecast(case_expr, switch_op_type);
538  }
539 }
540 
542 {
543  if(code.operands().size()!=3)
544  {
545  err_location(code);
546  error() << "gcc_switch_case_range expected to have three operands"
547  << eom;
548  throw 0;
549  }
550 
551  typecheck_code(to_code(code.op2()));
552 
553  if(!case_is_allowed)
554  {
555  err_location(code);
556  error() << "did not expect `case' here" << eom;
557  throw 0;
558  }
559 
560  typecheck_expr(code.op0());
561  typecheck_expr(code.op1());
564 }
565 
567 {
568  // these are just declarations, e.g.,
569  // __label__ here, there;
570 }
571 
573 {
574  // we record the label used
576 }
577 
579 {
580  if(code.operands().size()!=1)
581  {
582  err_location(code);
583  error() << "computed-goto expected to have one operand" << eom;
584  throw 0;
585  }
586 
587  exprt &dest=code.op0();
588 
589  if(dest.id()!=ID_dereference)
590  {
591  err_location(dest);
592  error() << "computed-goto expected to have dereferencing operand"
593  << eom;
594  throw 0;
595  }
596 
597  assert(dest.operands().size()==1);
598 
599  typecheck_expr(dest.op0());
600  dest.type()=empty_typet();
601 }
602 
604 {
605  if(code.operands().size()!=3)
606  {
607  err_location(code);
608  error() << "ifthenelse expected to have three operands" << eom;
609  throw 0;
610  }
611 
612  exprt &cond=code.cond();
613 
614  typecheck_expr(cond);
615 
616  #if 0
617  if(cond.id()==ID_sideeffect &&
618  cond.get(ID_statement)==ID_assign)
619  {
620  warning("warning: assignment in if condition");
621  }
622  #endif
623 
625 
626  if(to_code(code.then_case()).get_statement()==ID_decl_block)
627  {
628  code_blockt code_block;
629  code_block.add_source_location()=code.then_case().source_location();
630 
631  code_block.move_to_operands(code.then_case());
632  code.then_case().swap(code_block);
633  }
634 
636 
637  if(!code.else_case().is_nil())
638  {
639  if(to_code(code.else_case()).get_statement()==ID_decl_block)
640  {
641  code_blockt code_block;
642  code_block.add_source_location()=code.else_case().source_location();
643 
644  code_block.move_to_operands(code.else_case());
645  code.else_case().swap(code_block);
646  }
647 
649  }
650 }
651 
653 {
654  if(code.operands().size()!=1)
655  {
656  err_location(code);
657  error() << "start_thread expected to have one operand" << eom;
658  throw 0;
659  }
660 
661  typecheck_code(to_code(code.op0()));
662 }
663 
665 {
666  if(code.operands().empty())
667  {
668  if(follow(return_type).id()!=ID_empty &&
669  return_type.id()!=ID_constructor &&
670  return_type.id()!=ID_destructor)
671  {
672  // gcc doesn't actually complain, it just warns!
674  warning() << "non-void function should return a value" << eom;
675 
677  }
678  }
679  else if(code.operands().size()==1)
680  {
681  typecheck_expr(code.op0());
682 
683  if(follow(return_type).id()==ID_empty)
684  {
685  // gcc doesn't actually complain, it just warns!
686  if(follow(code.op0().type()).id()!=ID_empty)
687  {
689 
690  warning() << "function has return void ";
691  warning() << "but a return statement returning ";
692  warning() << to_string(follow(code.op0().type()));
693  warning() << eom;
694 
695  code.op0().make_typecast(return_type);
696  }
697  }
698  else
700  }
701  else
702  {
703  err_location(code);
704  error() << "return expected to have 0 or 1 operands" << eom;
705  throw 0;
706  }
707 }
708 
710 {
711  if(code.operands().size()!=2)
712  {
713  err_location(code);
714  error() << "switch expects two operands" << eom;
715  throw 0;
716  }
717 
718  typecheck_expr(code.value());
719 
720  // this needs to be promoted
722 
723  // save & set flags
724 
725  bool old_case_is_allowed(case_is_allowed);
726  bool old_break_is_allowed(break_is_allowed);
727  typet old_switch_op_type(switch_op_type);
728 
729  switch_op_type=code.value().type();
731 
732  typecheck_code(code.body());
733 
734  // restore flags
735  case_is_allowed=old_case_is_allowed;
736  break_is_allowed=old_break_is_allowed;
737  switch_op_type=old_switch_op_type;
738 }
739 
741 {
742  if(code.operands().size()!=2)
743  {
744  err_location(code);
745  error() << "while expected to have two operands" << eom;
746  throw 0;
747  }
748 
749  typecheck_expr(code.cond());
751 
752  // save & set flags
753  bool old_break_is_allowed(break_is_allowed);
754  bool old_continue_is_allowed(continue_is_allowed);
755 
757 
758  if(code.body().get_statement()==ID_decl_block)
759  {
760  code_blockt code_block;
761  code_block.add_source_location()=code.body().source_location();
762 
763  code_block.move_to_operands(code.body());
764  code.body().swap(code_block);
765  }
766  typecheck_code(code.body());
767 
768  // restore flags
769  break_is_allowed=old_break_is_allowed;
770  continue_is_allowed=old_continue_is_allowed;
771 
772  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
773 }
774 
776 {
777  if(code.operands().size()!=2)
778  {
779  err_location(code);
780  error() << "do while expected to have two operands" << eom;
781  throw 0;
782  }
783 
784  typecheck_expr(code.cond());
786 
787  // save & set flags
788  bool old_break_is_allowed(break_is_allowed);
789  bool old_continue_is_allowed(continue_is_allowed);
790 
792 
793  if(code.body().get_statement()==ID_decl_block)
794  {
795  code_blockt code_block;
796  code_block.add_source_location()=code.body().source_location();
797 
798  code_block.move_to_operands(code.body());
799  code.body().swap(code_block);
800  }
801  typecheck_code(code.body());
802 
803  // restore flags
804  break_is_allowed=old_break_is_allowed;
805  continue_is_allowed=old_continue_is_allowed;
806 
807  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
808 }
809 
811  codet &code,
812  const irep_idt &spec)
813 {
814  if(code.find(spec).is_not_nil())
815  {
816  exprt &constraint=
817  static_cast<exprt&>(code.add(spec));
818 
819  typecheck_expr(constraint);
820  implicit_typecast_bool(constraint);
821  }
822 }
const irep_idt & get_statement() const
Definition: std_code.h:39
bool get_is_static_assert() const
The type of an expression.
Definition: type.h:22
const codet & then_case() const
Definition: std_code.h:481
std::map< irep_idt, source_locationt > labels_used
struct configt::ansi_ct ansi_c
virtual void implicit_typecast_bool(exprt &expr)
virtual bool is_complete_type(const typet &type) const
virtual void typecheck_start_thread(codet &code)
A ‘switch’ instruction.
Definition: std_code.h:533
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
void typecheck_declaration(ansi_c_declarationt &)
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const exprt & cond() const
Definition: std_code.h:596
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_gcc_switch_case_range(codet &code)
const exprt & cond() const
Definition: std_code.h:471
exprt & symbol()
Definition: std_code.h:266
codet & code()
Definition: std_code.h:1048
const codet & body() const
Definition: std_code.h:661
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
source_locationt end_location() const
Definition: std_code.h:125
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
virtual void typecheck_switch_case(code_switch_caset &code)
A ‘goto’ instruction.
Definition: std_code.h:774
typet & type()
Definition: expr.h:56
const irep_idt & get_flavor() const
Definition: std_code.h:1155
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
virtual std::string to_string(const exprt &expr)
bool is_static_lifetime
Definition: symbol.h:67
const exprt & case_op() const
Definition: std_code.h:1038
symbol_tablet & symbol_table
mstreamt & warning() const
Definition: message.h:307
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:189
const declaratorst & declarators() const
virtual void typecheck_break(codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
The boolean constant true.
Definition: std_expr.h:4488
ANSI-C Language Type Checking.
A declaration of a local variable.
Definition: std_code.h:253
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_assign(codet &expr)
source_locationt source_location
Definition: message.h:214
The empty type.
Definition: std_types.h:54
codet & code()
Definition: std_code.h:979
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:682
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:627
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:807
virtual void typecheck_continue(codet &code)
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
A label for branch targets.
Definition: std_code.h:947
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
const exprt & size() const
Definition: std_types.h:1014
virtual void typecheck_expr(exprt &expr)
void err_location(const source_locationt &loc)
Definition: typecheck.h:27
bool for_has_scope
Definition: config.h:44
A ‘while’ instruction.
Definition: std_code.h:588
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1069
const typet & follow(const typet &) const
Definition: namespace.cpp:55
std::list< codet > clean_code
const symbolst & symbols
virtual void typecheck_switch(code_switcht &code)
virtual void typecheck_asm(codet &code)
virtual void typecheck_block(codet &code)
const codet & body() const
Definition: std_code.h:551
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:572
virtual void start_typecheck_code()
virtual void typecheck_for(codet &code)
virtual void typecheck_label(code_labelt &code)
bool is_extern
Definition: symbol.h:68
const exprt & value() const
Definition: std_code.h:541
virtual void implicit_typecast(exprt &expr, const typet &type)
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
virtual void typecheck_gcc_local_label(codet &code)
void set_statement(const irep_idt &statement)
Definition: std_code.h:34
bool is_default() const
Definition: std_code.h:1028
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_decl(codet &code)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
A ‘do while’ instruction.
Definition: std_code.h:643
const source_locationt & source_location() const
Definition: expr.h:125
ANSI-CC Language Type Checking.
irept & add(const irep_namet &name)
Definition: irep.cpp:306
std::map< irep_idt, source_locationt > labels_defined
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
const irep_idt & get_label() const
Definition: std_code.h:969
virtual void implicit_typecast_arithmetic(exprt &expr)
Skip.
Definition: std_code.h:178
An if-then-else.
Definition: std_code.h:461
exprt & op2()
Definition: expr.h:78
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
A switch-case.
Definition: std_code.h:1014
const irep_idt & get_destination() const
Definition: std_code.h:791
A statement in a programming language.
Definition: std_code.h:21
bool is_type
Definition: symbol.h:63
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1000
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
const exprt & cond() const
Definition: std_code.h:651
const codet & else_case() const
Definition: std_code.h:491
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:517
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const codet & body() const
Definition: std_code.h:606
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1174
virtual void typecheck_dowhile(code_dowhilet &code)
virtual void typecheck_return(codet &code)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void reserve_operands(operandst::size_type n)
Definition: expr.h:96
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_expression(codet &code)
exprt & op3()
Definition: expr.h:81