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>
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(unsigned 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::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  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!
673  // We'll put a zero here, which is dubious.
674  exprt zero=
677  code.copy_to_operands(zero);
678  }
679  }
680  else if(code.operands().size()==1)
681  {
682  typecheck_expr(code.op0());
683 
684  if(follow(return_type).id()==ID_empty)
685  {
686  // gcc doesn't actually complain, it just warns!
687  if(follow(code.op0().type()).id()!=ID_empty)
688  {
690 
691  warning() << "function has return void ";
692  warning() << "but a return statement returning ";
693  warning() << to_string(follow(code.op0().type()));
694  warning() << eom;
695 
696  code.op0().make_typecast(return_type);
697  }
698  }
699  else
701  }
702  else
703  {
704  err_location(code);
705  error() << "return expected to have 0 or 1 operands" << eom;
706  throw 0;
707  }
708 }
709 
711 {
712  if(code.operands().size()!=2)
713  {
714  err_location(code);
715  error() << "switch expects two operands" << eom;
716  throw 0;
717  }
718 
719  typecheck_expr(code.value());
720 
721  // this needs to be promoted
723 
724  // save & set flags
725 
726  bool old_case_is_allowed(case_is_allowed);
727  bool old_break_is_allowed(break_is_allowed);
728  typet old_switch_op_type(switch_op_type);
729 
730  switch_op_type=code.value().type();
732 
733  typecheck_code(code.body());
734 
735  // restore flags
736  case_is_allowed=old_case_is_allowed;
737  break_is_allowed=old_break_is_allowed;
738  switch_op_type=old_switch_op_type;
739 }
740 
742 {
743  if(code.operands().size()!=2)
744  {
745  err_location(code);
746  error() << "while expected to have two operands" << eom;
747  throw 0;
748  }
749 
750  typecheck_expr(code.cond());
752 
753  // save & set flags
754  bool old_break_is_allowed(break_is_allowed);
755  bool old_continue_is_allowed(continue_is_allowed);
756 
758 
759  if(code.body().get_statement()==ID_decl_block)
760  {
761  code_blockt code_block;
762  code_block.add_source_location()=code.body().source_location();
763 
764  code_block.move_to_operands(code.body());
765  code.body().swap(code_block);
766  }
767  typecheck_code(code.body());
768 
769  // restore flags
770  break_is_allowed=old_break_is_allowed;
771  continue_is_allowed=old_continue_is_allowed;
772 
773  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
774 }
775 
777 {
778  if(code.operands().size()!=2)
779  {
780  err_location(code);
781  error() << "do while expected to have two operands" << eom;
782  throw 0;
783  }
784 
785  typecheck_expr(code.cond());
787 
788  // save & set flags
789  bool old_break_is_allowed(break_is_allowed);
790  bool old_continue_is_allowed(continue_is_allowed);
791 
793 
794  if(code.body().get_statement()==ID_decl_block)
795  {
796  code_blockt code_block;
797  code_block.add_source_location()=code.body().source_location();
798 
799  code_block.move_to_operands(code.body());
800  code.body().swap(code_block);
801  }
802  typecheck_code(code.body());
803 
804  // restore flags
805  break_is_allowed=old_break_is_allowed;
806  continue_is_allowed=old_continue_is_allowed;
807 
808  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
809 }
810 
812  codet &code,
813  const irep_idt &spec)
814 {
815  if(code.find(spec).is_not_nil())
816  {
817  exprt &constraint=
818  static_cast<exprt&>(code.add(spec));
819 
820  typecheck_expr(constraint);
821  implicit_typecast_bool(constraint);
822  }
823 }
const irep_idt & get_statement() const
Definition: std_code.h:37
bool get_is_static_assert() const
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
const codet & then_case() const
Definition: std_code.h:370
std::map< irep_idt, source_locationt > labels_used
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
virtual void implicit_typecast_bool(exprt &expr)
virtual bool is_complete_type(const typet &type) const
Linking: Zero Initialization.
virtual void typecheck_start_thread(codet &code)
A ‘switch’ instruction.
Definition: std_code.h:412
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:734
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const exprt & cond() const
Definition: std_code.h:465
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_gcc_switch_case_range(codet &code)
const exprt & cond() const
Definition: std_code.h:360
exprt & symbol()
Definition: std_code.h:205
codet & code()
Definition: std_code.h:851
const codet & body() const
Definition: std_code.h:520
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
source_locationt end_location() const
Definition: std_code.h:89
std::vector< componentt > componentst
Definition: std_types.h:240
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
exprt value
Initial value of symbol.
Definition: symbol.h:40
const componentst & components() const
Definition: std_types.h:242
virtual void typecheck_switch_case(code_switch_caset &code)
A ‘goto’ instruction.
Definition: std_code.h:613
typet & type()
Definition: expr.h:60
const irep_idt & get_flavor() const
Definition: std_code.h:932
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
virtual std::string to_string(const exprt &expr)
bool is_static_lifetime
Definition: symbol.h:70
const exprt & case_op() const
Definition: std_code.h:841
symbol_tablet & symbol_table
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const irep_idt & id() const
Definition: irep.h:189
const declaratorst & declarators() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
virtual void typecheck_break(codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
The boolean constant true.
Definition: std_expr.h:3742
symbolst symbols
Definition: symbol_table.h:57
ANSI-C Language Type Checking.
A declaration of a local variable.
Definition: std_code.h:192
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_assign(codet &expr)
source_locationt source_location
Definition: message.h:175
The empty type.
Definition: std_types.h:53
codet & code()
Definition: std_code.h:792
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:531
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:486
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:636
virtual void typecheck_continue(codet &code)
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
A label for branch targets.
Definition: std_code.h:760
const exprt & size() const
Definition: std_types.h:915
virtual void typecheck_expr(exprt &expr)
void err_location(const source_locationt &loc)
Definition: typecheck.h:27
bool for_has_scope
Definition: config.h:45
A ‘while’ instruction.
Definition: std_code.h:457
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:862
std::list< codet > clean_code
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:430
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:441
virtual void start_typecheck_code()
virtual void typecheck_for(codet &code)
virtual void typecheck_label(code_labelt &code)
bool is_extern
Definition: symbol.h:71
const exprt & value() const
Definition: std_code.h:420
virtual void implicit_typecast(exprt &expr, const typet &type)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
message_handlert & get_message_handler()
Definition: message.h:127
virtual void typecheck_gcc_local_label(codet &code)
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
bool is_default() const
Definition: std_code.h:831
Base class for all expressions.
Definition: expr.h:46
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_decl(codet &code)
A ‘do while’ instruction.
Definition: std_code.h:502
const source_locationt & source_location() const
Definition: expr.h:142
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
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
const irep_idt & get_label() const
Definition: std_code.h:782
virtual void implicit_typecast_arithmetic(exprt &expr)
Skip.
Definition: std_code.h:134
An if-then-else.
Definition: std_code.h:350
exprt & op2()
Definition: expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
A switch-case.
Definition: std_code.h:817
const irep_idt & get_destination() const
Definition: std_code.h:630
A statement in a programming language.
Definition: std_code.h:19
bool is_type
Definition: symbol.h:66
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:803
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
const exprt & cond() const
Definition: std_code.h:510
const codet & else_case() const
Definition: std_code.h:380
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:396
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const codet & body() const
Definition: std_code.h:475
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:943
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:108
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_expression(codet &code)
exprt & op3()
Definition: expr.h:93