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(symbol.symbol_expr());
326  code.add_source_location()=symbol.location;
327  code.symbol().add_source_location()=symbol.location;
328 
329  // add initializer, if any
330  if(symbol.value.is_not_nil())
331  {
332  code.operands().resize(2);
333  code.op1()=symbol.value;
334  }
335 
336  new_code.push_back(code);
337  }
338  }
339 
340  // stash away any side-effects in the declaration
341  new_code.splice(new_code.begin(), clean_code);
342 
343  if(new_code.empty())
344  {
345  source_locationt source_location=code.source_location();
346  code=code_skipt();
347  code.add_source_location()=source_location;
348  }
349  else if(new_code.size()==1)
350  {
351  code.swap(new_code.front());
352  }
353  else
354  {
355  // build a decl-block
356  code_blockt code_block(new_code);
357  code_block.set_statement(ID_decl_block);
358  code.swap(code_block);
359  }
360 }
361 
363 {
364  if(type.id()==ID_incomplete_struct ||
365  type.id()==ID_incomplete_union)
366  return false;
367  else if(type.id()==ID_array)
368  {
369  if(to_array_type(type).size().is_nil())
370  return false;
371  return is_complete_type(type.subtype());
372  }
373  else if(type.id()==ID_struct || type.id()==ID_union)
374  {
375  const struct_union_typet::componentst &components=
377  for(struct_union_typet::componentst::const_iterator
378  it=components.begin();
379  it!=components.end();
380  it++)
381  if(!is_complete_type(it->type()))
382  return false;
383  }
384  else if(type.id()==ID_vector)
385  return is_complete_type(type.subtype());
386  else if(type.id()==ID_symbol)
387  return is_complete_type(follow(type));
388 
389  return true;
390 }
391 
393 {
394  if(code.operands().size()!=1)
395  {
396  err_location(code);
397  error() << "expression statement expected to have one operand"
398  << eom;
399  throw 0;
400  }
401 
402  exprt &op=code.op0();
403  typecheck_expr(op);
404 }
405 
407 {
408  if(code.operands().size()!=4)
409  {
410  err_location(code);
411  error() << "for expected to have four operands" << eom;
412  throw 0;
413  }
414 
415  // the "for" statement has an implicit block around it,
416  // since code.op0() may contain declarations
417  //
418  // we therefore transform
419  //
420  // for(a;b;c) d;
421  //
422  // to
423  //
424  // { a; for(;b;c) d; }
425  //
426  // if config.ansi_c.for_has_scope
427 
429  code.op0().is_nil())
430  {
431  if(code.op0().is_not_nil())
432  typecheck_code(to_code(code.op0()));
433 
434  if(code.op1().is_nil())
435  code.op1()=true_exprt();
436  else
437  {
438  typecheck_expr(code.op1());
439  implicit_typecast_bool(code.op1());
440  }
441 
442  if(code.op2().is_not_nil())
443  typecheck_expr(code.op2());
444 
445  if(code.op3().is_not_nil())
446  {
447  // save & set flags
448  bool old_break_is_allowed=break_is_allowed;
449  bool old_continue_is_allowed=continue_is_allowed;
450 
452 
453  // recursive call
454  if(to_code(code.op3()).get_statement()==ID_decl_block)
455  {
456  code_blockt code_block;
457  code_block.add_source_location()=code.op3().source_location();
458 
459  code_block.move_to_operands(code.op3());
460  code.op3().swap(code_block);
461  }
462  typecheck_code(to_code(code.op3()));
463 
464  // restore flags
465  break_is_allowed=old_break_is_allowed;
466  continue_is_allowed=old_continue_is_allowed;
467  }
468  }
469  else
470  {
471  code_blockt code_block;
472  code_block.add_source_location()=code.source_location();
473  if(to_code(code.op3()).get_statement()==ID_block)
474  {
475  code_block.set(
476  ID_C_end_location,
478  }
479  else
480  {
481  code_block.set(
482  ID_C_end_location,
483  code.op3().source_location());
484  }
485 
486  code_block.reserve_operands(2);
487  code_block.move_to_operands(code.op0());
488  code.op0().make_nil();
489  code_block.move_to_operands(code);
490  code.swap(code_block);
491  typecheck_code(code); // recursive call
492  }
493 
494  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
495 }
496 
498 {
499  // record the label
501 
502  typecheck_code(code.code());
503 }
504 
506 {
507  if(code.operands().size()!=2)
508  {
509  err_location(code);
510  error() << "switch_case expected to have two operands" << eom;
511  throw 0;
512  }
513 
514  typecheck_code(code.code());
515 
516  if(code.is_default())
517  {
518  if(!case_is_allowed)
519  {
520  err_location(code);
521  error() << "did not expect default label here" << eom;
522  throw 0;
523  }
524  }
525  else
526  {
527  if(!case_is_allowed)
528  {
529  err_location(code);
530  error() << "did not expect `case' here" << eom;
531  throw 0;
532  }
533 
534  exprt &case_expr=code.case_op();
535  typecheck_expr(case_expr);
536  implicit_typecast(case_expr, switch_op_type);
537  make_constant(case_expr);
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  make_constant(code.op0());
565  make_constant(code.op1());
566 }
567 
569 {
570  // these are just declarations, e.g.,
571  // __label__ here, there;
572 }
573 
575 {
576  // we record the label used
578 }
579 
581 {
582  if(code.operands().size()!=1)
583  {
584  err_location(code);
585  error() << "computed-goto expected to have one operand" << eom;
586  throw 0;
587  }
588 
589  exprt &dest=code.op0();
590 
591  if(dest.id()!=ID_dereference)
592  {
593  err_location(dest);
594  error() << "computed-goto expected to have dereferencing operand"
595  << eom;
596  throw 0;
597  }
598 
599  assert(dest.operands().size()==1);
600 
601  typecheck_expr(dest.op0());
602  dest.type()=empty_typet();
603 }
604 
606 {
607  if(code.operands().size()!=3)
608  {
609  err_location(code);
610  error() << "ifthenelse expected to have three operands" << eom;
611  throw 0;
612  }
613 
614  exprt &cond=code.cond();
615 
616  typecheck_expr(cond);
617 
618  #if 0
619  if(cond.id()==ID_sideeffect &&
620  cond.get(ID_statement)==ID_assign)
621  {
622  warning("warning: assignment in if condition");
623  }
624  #endif
625 
627 
628  if(code.then_case().get_statement() == ID_decl_block)
629  {
630  code_blockt code_block;
631  code_block.add_source_location()=code.then_case().source_location();
632 
633  code_block.move_to_operands(code.then_case());
634  code.then_case().swap(code_block);
635  }
636 
637  typecheck_code(code.then_case());
638 
639  if(!code.else_case().is_nil())
640  {
641  if(code.else_case().get_statement() == ID_decl_block)
642  {
643  code_blockt code_block;
644  code_block.add_source_location()=code.else_case().source_location();
645 
646  code_block.move_to_operands(code.else_case());
647  code.else_case().swap(code_block);
648  }
649 
650  typecheck_code(code.else_case());
651  }
652 }
653 
655 {
656  if(code.operands().size()!=1)
657  {
658  err_location(code);
659  error() << "start_thread expected to have one operand" << eom;
660  throw 0;
661  }
662 
663  typecheck_code(to_code(code.op0()));
664 }
665 
667 {
668  if(code.operands().empty())
669  {
670  if(follow(return_type).id()!=ID_empty &&
671  return_type.id()!=ID_constructor &&
672  return_type.id()!=ID_destructor)
673  {
674  // gcc doesn't actually complain, it just warns!
676  warning() << "non-void function should return a value" << eom;
677 
678  code.copy_to_operands(
680  }
681  }
682  else if(code.operands().size()==1)
683  {
684  typecheck_expr(code.op0());
685 
686  if(follow(return_type).id()==ID_empty)
687  {
688  // gcc doesn't actually complain, it just warns!
689  if(follow(code.op0().type()).id()!=ID_empty)
690  {
692 
693  warning() << "function has return void ";
694  warning() << "but a return statement returning ";
695  warning() << to_string(follow(code.op0().type()));
696  warning() << eom;
697 
698  code.op0().make_typecast(return_type);
699  }
700  }
701  else
703  }
704  else
705  {
706  err_location(code);
707  error() << "return expected to have 0 or 1 operands" << eom;
708  throw 0;
709  }
710 }
711 
713 {
714  if(code.operands().size()!=2)
715  {
716  err_location(code);
717  error() << "switch expects two operands" << eom;
718  throw 0;
719  }
720 
721  typecheck_expr(code.value());
722 
723  // this needs to be promoted
725 
726  // save & set flags
727 
728  bool old_case_is_allowed(case_is_allowed);
729  bool old_break_is_allowed(break_is_allowed);
730  typet old_switch_op_type(switch_op_type);
731 
732  switch_op_type=code.value().type();
734 
735  typecheck_code(code.body());
736 
737  // restore flags
738  case_is_allowed=old_case_is_allowed;
739  break_is_allowed=old_break_is_allowed;
740  switch_op_type=old_switch_op_type;
741 }
742 
744 {
745  if(code.operands().size()!=2)
746  {
747  err_location(code);
748  error() << "while expected to have two operands" << eom;
749  throw 0;
750  }
751 
752  typecheck_expr(code.cond());
754 
755  // save & set flags
756  bool old_break_is_allowed(break_is_allowed);
757  bool old_continue_is_allowed(continue_is_allowed);
758 
760 
761  if(code.body().get_statement()==ID_decl_block)
762  {
763  code_blockt code_block;
764  code_block.add_source_location()=code.body().source_location();
765 
766  code_block.move_to_operands(code.body());
767  code.body().swap(code_block);
768  }
769  typecheck_code(code.body());
770 
771  // restore flags
772  break_is_allowed=old_break_is_allowed;
773  continue_is_allowed=old_continue_is_allowed;
774 
775  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
776 }
777 
779 {
780  if(code.operands().size()!=2)
781  {
782  err_location(code);
783  error() << "do while expected to have two operands" << eom;
784  throw 0;
785  }
786 
787  typecheck_expr(code.cond());
789 
790  // save & set flags
791  bool old_break_is_allowed(break_is_allowed);
792  bool old_continue_is_allowed(continue_is_allowed);
793 
795 
796  if(code.body().get_statement()==ID_decl_block)
797  {
798  code_blockt code_block;
799  code_block.add_source_location()=code.body().source_location();
800 
801  code_block.move_to_operands(code.body());
802  code.body().swap(code_block);
803  }
804  typecheck_code(code.body());
805 
806  // restore flags
807  break_is_allowed=old_break_is_allowed;
808  continue_is_allowed=old_continue_is_allowed;
809 
810  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
811 }
812 
814  codet &code,
815  const irep_idt &spec)
816 {
817  if(code.find(spec).is_not_nil())
818  {
819  exprt &constraint=
820  static_cast<exprt&>(code.add(spec));
821 
822  typecheck_expr(constraint);
823  implicit_typecast_bool(constraint);
824  }
825 }
const irep_idt & get_statement() const
Definition: std_code.h:40
bool get_is_static_assert() const
The type of an expression.
Definition: type.h:22
const codet & then_case() const
Definition: std_code.h:486
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:538
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:172
bool is_not_nil() const
Definition: irep.h:173
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:617
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_gcc_switch_case_range(codet &code)
virtual void make_constant(exprt &expr)
const exprt & cond() const
Definition: std_code.h:476
codet & code()
Definition: std_code.h:1080
const codet & body() const
Definition: std_code.h:690
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
source_locationt end_location() const
Definition: std_code.h:126
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:803
typet & type()
Definition: expr.h:56
const irep_idt & get_flavor() const
Definition: std_code.h:1187
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:1070
symbol_tablet & symbol_table
mstreamt & warning() const
Definition: message.h:307
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
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:4486
ANSI-C Language Type Checking.
A declaration of a local variable.
Definition: std_code.h:254
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:1010
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:711
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:648
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:837
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:977
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
const exprt & size() const
Definition: std_types.h:1023
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:601
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1101
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:564
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:585
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:554
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:35
bool is_default() const
Definition: std_code.h:1060
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
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:664
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:315
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
const irep_idt & get_label() const
Definition: std_code.h:1000
virtual void implicit_typecast_arithmetic(exprt &expr)
Skip.
Definition: std_code.h:179
An if-then-else.
Definition: std_code.h:466
exprt & op2()
Definition: expr.h:78
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
A switch-case.
Definition: std_code.h:1045
const irep_idt & get_destination() const
Definition: std_code.h:821
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:1031
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
const exprt & cond() const
Definition: std_code.h:680
const codet & else_case() const
Definition: std_code.h:496
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:522
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const codet & body() const
Definition: std_code.h:627
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1206
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:286
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