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/c_types.h>
15 #include <util/config.h>
16 #include <util/expr_initializer.h>
17 #include <util/range.h>
18 
19 #include "ansi_c_declaration.h"
20 
22 {
24 }
25 
27 {
28  if(code.id()!=ID_code)
29  {
31  error() << "expected code, got " << code.pretty() << eom;
32  throw 0;
33  }
34 
35  code.type() = empty_typet();
36 
37  const irep_idt &statement=code.get_statement();
38 
39  if(statement==ID_expression)
41  else if(statement==ID_label)
43  else if(statement==ID_switch_case)
45  else if(statement==ID_gcc_switch_case_range)
47  else if(statement==ID_block)
49  else if(statement==ID_decl_block)
50  {
51  }
52  else if(statement==ID_ifthenelse)
54  else if(statement==ID_while)
56  else if(statement==ID_dowhile)
58  else if(statement==ID_for)
59  typecheck_for(code);
60  else if(statement==ID_switch)
61  typecheck_switch(code);
62  else if(statement==ID_break)
63  typecheck_break(code);
64  else if(statement==ID_goto)
66  else if(statement==ID_gcc_computed_goto)
68  else if(statement==ID_continue)
69  typecheck_continue(code);
70  else if(statement==ID_return)
72  else if(statement==ID_decl)
73  typecheck_decl(code);
74  else if(statement==ID_assign)
75  typecheck_assign(code);
76  else if(statement==ID_skip)
77  {
78  }
79  else if(statement==ID_asm)
81  else if(statement==ID_start_thread)
83  else if(statement==ID_gcc_local_label)
85  else if(statement==ID_msc_try_finally)
86  {
87  assert(code.operands().size()==2);
88  typecheck_code(to_code(code.op0()));
89  typecheck_code(to_code(code.op1()));
90  }
91  else if(statement==ID_msc_try_except)
92  {
93  assert(code.operands().size()==3);
94  typecheck_code(to_code(code.op0()));
95  typecheck_expr(code.op1());
96  typecheck_code(to_code(code.op2()));
97  }
98  else if(statement==ID_msc_leave)
99  {
100  // fine as is, but should check that we
101  // are in a 'try' block
102  }
103  else if(statement==ID_static_assert)
104  {
105  assert(code.operands().size()==2);
106  typecheck_expr(code.op0());
107  typecheck_expr(code.op1());
108  }
109  else if(statement==ID_CPROVER_try_catch ||
110  statement==ID_CPROVER_try_finally)
111  {
112  assert(code.operands().size()==2);
113  typecheck_code(to_code(code.op0()));
114  typecheck_code(to_code(code.op1()));
115  }
116  else if(statement==ID_CPROVER_throw)
117  {
118  assert(code.operands().empty());
119  }
120  else if(statement==ID_assume ||
121  statement==ID_assert)
122  {
123  // These are not generated by the C/C++ parsers,
124  // but we allow them for the benefit of other users
125  // of the typechecker.
126  assert(code.operands().size()==1);
127  typecheck_expr(code.op0());
128  }
129  else
130  {
132  error() << "unexpected statement: " << statement << eom;
133  throw 0;
134  }
135 }
136 
138 {
139  const irep_idt flavor = code.get_flavor();
140 
141  if(flavor==ID_gcc)
142  {
143  // These have 5 operands.
144  // The first operand is a string.
145  // Operands 1, 2, 3, 4 are lists of expressions.
146 
147  // Operand 1: OutputOperands
148  // Operand 2: InputOperands
149  // Operand 3: Clobbers
150  // Operand 4: GotoLabels
151 
152  auto &code_asm_gcc = to_code_asm_gcc(code);
153 
154  typecheck_expr(code_asm_gcc.asm_text());
155 
156  // the operands are lists of expressions
157  for(auto &op : ranget<exprt::operandst::iterator>(
158  code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
159  {
160  for(auto &expr : op.operands())
161  typecheck_expr(expr);
162  }
163  }
164  else if(flavor==ID_msc)
165  {
166  assert(code.operands().size()==1);
167  typecheck_expr(code.op0());
168  }
169 }
170 
172 {
173  if(code.operands().size()!=2)
174  {
176  error() << "assignment statement expected to have two operands"
177  << eom;
178  throw 0;
179  }
180 
181  typecheck_expr(code.op0());
182  typecheck_expr(code.op1());
183 
184  implicit_typecast(code.op1(), code.op0().type());
185 }
186 
188 {
189  for(auto &c : code.statements())
190  typecheck_code(c);
191 
192  // do decl-blocks
193 
194  code_blockt new_ops;
195  new_ops.statements().reserve(code.statements().size());
196 
197  for(auto &code_op : code.statements())
198  {
199  if(code_op.is_not_nil())
200  new_ops.add(std::move(code_op));
201  }
202 
203  code.statements().swap(new_ops.statements());
204 }
205 
207 {
208  if(!break_is_allowed)
209  {
211  error() << "break not allowed here" << eom;
212  throw 0;
213  }
214 }
215 
217 {
219  {
221  error() << "continue not allowed here" << eom;
222  throw 0;
223  }
224 }
225 
227 {
228  // this comes with 1 operand, which is a declaration
229  if(code.operands().size()!=1)
230  {
232  error() << "decl expected to have 1 operand" << eom;
233  throw 0;
234  }
235 
236  // op0 must be declaration
237  if(code.op0().id()!=ID_declaration)
238  {
240  error() << "decl statement expected to have declaration as operand"
241  << eom;
242  throw 0;
243  }
244 
245  ansi_c_declarationt declaration;
246  declaration.swap(code.op0());
247 
248  if(declaration.get_is_static_assert())
249  {
250  assert(declaration.operands().size()==2);
251  codet new_code(ID_static_assert);
252  new_code.add_source_location()=code.source_location();
253  new_code.operands().swap(declaration.operands());
254  code.swap(new_code);
255  typecheck_code(code);
256  return; // done
257  }
258 
259  typecheck_declaration(declaration);
260 
261  std::list<codet> new_code;
262 
263  // iterate over declarators
264 
265  for(const auto &d : declaration.declarators())
266  {
267  irep_idt identifier = d.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_array)
345  {
346  if(to_array_type(type).size().is_nil())
347  return false;
348  return is_complete_type(type.subtype());
349  }
350  else if(type.id()==ID_struct || type.id()==ID_union)
351  {
352  const auto &struct_union_type = to_struct_union_type(type);
353 
354  if(struct_union_type.is_incomplete())
355  return false;
356 
357  for(const auto &c : struct_union_type.components())
358  if(!is_complete_type(c.type()))
359  return false;
360  }
361  else if(type.id()==ID_vector)
362  return is_complete_type(type.subtype());
363  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
364  {
365  return is_complete_type(follow(type));
366  }
367 
368  return true;
369 }
370 
372 {
373  if(code.operands().size()!=1)
374  {
376  error() << "expression statement expected to have one operand"
377  << eom;
378  throw 0;
379  }
380 
381  exprt &op=code.op0();
382  typecheck_expr(op);
383 }
384 
386 {
387  if(code.operands().size()!=4)
388  {
390  error() << "for expected to have four operands" << eom;
391  throw 0;
392  }
393 
394  // the "for" statement has an implicit block around it,
395  // since code.op0() may contain declarations
396  //
397  // we therefore transform
398  //
399  // for(a;b;c) d;
400  //
401  // to
402  //
403  // { a; for(;b;c) d; }
404  //
405  // if config.ansi_c.for_has_scope
406 
408  code.op0().is_nil())
409  {
410  if(code.op0().is_not_nil())
411  typecheck_code(to_code(code.op0()));
412 
413  if(code.op1().is_nil())
414  code.op1()=true_exprt();
415  else
416  {
417  typecheck_expr(code.op1());
418  implicit_typecast_bool(code.op1());
419  }
420 
421  if(code.op2().is_not_nil())
422  typecheck_expr(code.op2());
423 
424  if(code.op3().is_not_nil())
425  {
426  // save & set flags
427  bool old_break_is_allowed=break_is_allowed;
428  bool old_continue_is_allowed=continue_is_allowed;
429 
431 
432  // recursive call
433  if(to_code(code.op3()).get_statement()==ID_decl_block)
434  {
435  code_blockt code_block;
436  code_block.add_source_location()=code.op3().source_location();
437 
438  code_block.add(std::move(to_code(code.op3())));
439  code.op3().swap(code_block);
440  }
441  typecheck_code(to_code(code.op3()));
442 
443  // restore flags
444  break_is_allowed=old_break_is_allowed;
445  continue_is_allowed=old_continue_is_allowed;
446  }
447  }
448  else
449  {
450  code_blockt code_block;
451  code_block.add_source_location()=code.source_location();
452  if(to_code(code.op3()).get_statement()==ID_block)
453  {
454  code_block.set(
455  ID_C_end_location,
457  }
458  else
459  {
460  code_block.set(
461  ID_C_end_location,
462  code.op3().source_location());
463  }
464 
465  code_block.reserve_operands(2);
466  code_block.add(std::move(to_code(code.op0())));
467  code.op0().make_nil();
468  code_block.add(std::move(code));
469  code.swap(code_block);
470  typecheck_code(code); // recursive call
471  }
472 
473  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
474 }
475 
477 {
478  // record the label
480 
481  typecheck_code(code.code());
482 }
483 
485 {
486  if(code.operands().size()!=2)
487  {
489  error() << "switch_case expected to have two operands" << eom;
490  throw 0;
491  }
492 
493  typecheck_code(code.code());
494 
495  if(code.is_default())
496  {
497  if(!case_is_allowed)
498  {
500  error() << "did not expect default label here" << eom;
501  throw 0;
502  }
503  }
504  else
505  {
506  if(!case_is_allowed)
507  {
509  error() << "did not expect `case' here" << eom;
510  throw 0;
511  }
512 
513  exprt &case_expr=code.case_op();
514  typecheck_expr(case_expr);
515  implicit_typecast(case_expr, switch_op_type);
516  make_constant(case_expr);
517  }
518 }
519 
522 {
523  if(!case_is_allowed)
524  {
526  error() << "did not expect `case' here" << eom;
527  throw 0;
528  }
529 
530  typecheck_expr(code.lower());
531  typecheck_expr(code.upper());
534  make_constant(code.lower());
535  make_constant(code.upper());
536  typecheck_code(code.code());
537 }
538 
540 {
541  // these are just declarations, e.g.,
542  // __label__ here, there;
543 }
544 
546 {
547  // we record the label used
549 }
550 
552 {
553  if(code.operands().size()!=1)
554  {
556  error() << "computed-goto expected to have one operand" << eom;
557  throw 0;
558  }
559 
560  exprt &dest=code.op0();
561 
562  if(dest.id()!=ID_dereference)
563  {
565  error() << "computed-goto expected to have dereferencing operand"
566  << eom;
567  throw 0;
568  }
569 
570  typecheck_expr(to_unary_expr(dest).op());
571  dest.type() = void_type();
572 }
573 
575 {
576  if(code.operands().size()!=3)
577  {
579  error() << "ifthenelse expected to have three operands" << eom;
580  throw 0;
581  }
582 
583  exprt &cond=code.cond();
584 
585  typecheck_expr(cond);
586 
587  #if 0
588  if(cond.id()==ID_sideeffect &&
589  cond.get(ID_statement)==ID_assign)
590  {
591  warning("warning: assignment in if condition");
592  }
593  #endif
594 
596 
597  if(code.then_case().get_statement() == ID_decl_block)
598  {
599  code_blockt code_block({code.then_case()});
600  code_block.add_source_location()=code.then_case().source_location();
601  code.then_case() = code_block;
602  }
603 
604  typecheck_code(code.then_case());
605 
606  if(!code.else_case().is_nil())
607  {
608  if(code.else_case().get_statement() == ID_decl_block)
609  {
610  code_blockt code_block({code.else_case()});
611  code_block.add_source_location()=code.else_case().source_location();
612  code.else_case() = code_block;
613  }
614 
615  typecheck_code(code.else_case());
616  }
617 }
618 
620 {
621  if(code.operands().size()!=1)
622  {
624  error() << "start_thread expected to have one operand" << eom;
625  throw 0;
626  }
627 
628  typecheck_code(to_code(code.op0()));
629 }
630 
632 {
633  if(code.has_return_value())
634  {
636 
637  if(return_type.id() == ID_empty)
638  {
639  // gcc doesn't actually complain, it just warns!
640  if(code.return_value().type().id() != ID_empty)
641  {
643 
644  warning() << "function has return void ";
645  warning() << "but a return statement returning ";
646  warning() << to_string(code.return_value().type());
647  warning() << eom;
648 
650  }
651  }
652  else
654  }
655  else if(
656  return_type.id() != ID_empty && return_type.id() != ID_constructor &&
657  return_type.id() != ID_destructor)
658  {
659  // gcc doesn't actually complain, it just warns!
661  warning() << "non-void function should return a value" << eom;
662 
663  code.return_value() =
665  }
666 }
667 
669 {
670  // we expect a code_switcht, but might return either a code_switcht or a
671  // code_blockt, hence don't use code_switcht in the interface
672  code_switcht &code_switch = to_code_switch(code);
673 
674  typecheck_expr(code_switch.value());
675 
676  // this needs to be promoted
677  implicit_typecast_arithmetic(code_switch.value());
678 
679  // save & set flags
680 
681  bool old_case_is_allowed(case_is_allowed);
682  bool old_break_is_allowed(break_is_allowed);
683  typet old_switch_op_type(switch_op_type);
684 
685  switch_op_type = code_switch.value().type();
687 
688  typecheck_code(code_switch.body());
689 
690  if(code_switch.body().get_statement() == ID_block)
691  {
692  // Collect all declarations before the first case, if there is any case
693  // (including a default one).
694  code_blockt wrapping_block;
695 
696  code_blockt &body_block = to_code_block(code_switch.body());
697  for(auto &statement : body_block.statements())
698  {
699  if(statement.get_statement() == ID_switch_case)
700  break;
701  else if(statement.get_statement() == ID_decl)
702  {
703  if(statement.operands().size() == 1)
704  {
705  wrapping_block.add(code_skipt());
706  wrapping_block.statements().back().swap(statement);
707  }
708  else
709  {
710  PRECONDITION(statement.operands().size() == 2);
711  wrapping_block.add(statement);
712  wrapping_block.statements().back().operands().pop_back();
713  statement.set_statement(ID_assign);
714  }
715  }
716  }
717 
718  if(!wrapping_block.statements().empty())
719  {
720  wrapping_block.add(std::move(code));
721  code.swap(wrapping_block);
722  }
723  }
724 
725  // restore flags
726  case_is_allowed=old_case_is_allowed;
727  break_is_allowed=old_break_is_allowed;
728  switch_op_type=old_switch_op_type;
729 }
730 
732 {
733  if(code.operands().size()!=2)
734  {
736  error() << "while expected to have two operands" << eom;
737  throw 0;
738  }
739 
740  typecheck_expr(code.cond());
742 
743  // save & set flags
744  bool old_break_is_allowed(break_is_allowed);
745  bool old_continue_is_allowed(continue_is_allowed);
746 
748 
749  if(code.body().get_statement()==ID_decl_block)
750  {
751  code_blockt code_block({code.body()});
752  code_block.add_source_location()=code.body().source_location();
753  code.body() = code_block;
754  }
755  typecheck_code(code.body());
756 
757  // restore flags
758  break_is_allowed=old_break_is_allowed;
759  continue_is_allowed=old_continue_is_allowed;
760 
761  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
762 }
763 
765 {
766  if(code.operands().size()!=2)
767  {
769  error() << "do while expected to have two operands" << eom;
770  throw 0;
771  }
772 
773  typecheck_expr(code.cond());
775 
776  // save & set flags
777  bool old_break_is_allowed(break_is_allowed);
778  bool old_continue_is_allowed(continue_is_allowed);
779 
781 
782  if(code.body().get_statement()==ID_decl_block)
783  {
784  code_blockt code_block({code.body()});
785  code_block.add_source_location()=code.body().source_location();
786  code.body() = code_block;
787  }
788  typecheck_code(code.body());
789 
790  // restore flags
791  break_is_allowed=old_break_is_allowed;
792  continue_is_allowed=old_continue_is_allowed;
793 
794  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
795 }
796 
798 {
799  if(code.find(spec).is_not_nil())
800  {
801  exprt &constraint = static_cast<exprt &>(code.add(spec));
802 
803  typecheck_expr(constraint);
804  implicit_typecast_bool(constraint);
805  }
806 }
807 
809  const code_typet &function_declarator,
810  const irept &contract)
811 {
812  exprt assigns = static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
813 
814  // Make sure there is an assigns clause to check
815  if(assigns.is_not_nil())
816  {
817  for(const auto &curr_param : function_declarator.parameters())
818  {
819  if(curr_param.id() == ID_declaration)
820  {
821  const ansi_c_declarationt &param_declaration =
822  to_ansi_c_declaration(curr_param);
823 
824  for(const auto &decl : param_declaration.declarators())
825  {
826  typecheck_assigns(decl, assigns);
827  }
828  }
829  }
830  }
831 }
832 
834  const ansi_c_declaratort &declarator,
835  const exprt &assigns)
836 {
837  for(exprt curr_op : assigns.operands())
838  {
839  if(curr_op.id() != ID_symbol)
840  {
841  continue;
842  }
843  const symbol_exprt &symbol_op = to_symbol_expr(curr_op);
844 
845  if(symbol_op.get(ID_C_base_name) == declarator.get_base_name())
846  {
847  error().source_location = declarator.source_location();
848  error() << "Formal parameter " << declarator.get_name() << " without "
849  << "dereference appears in ASSIGNS clause. Assigning this "
850  << "parameter will never affect the state of the calling context."
851  << " Did you mean to write *" << declarator.get_name() << "?"
852  << eom;
853  throw 0;
854  }
855  }
856 }
857 
859  codet &code,
860  const irep_idt &spec)
861 {
862  if(code.find(spec).is_not_nil())
863  {
864  exprt &constraint = static_cast<exprt &>(code.add(spec));
865 
866  typecheck_expr(constraint);
867  }
868 }
c_typecheck_baset::typecheck_assigns_exprs
virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:858
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_switch_caset::case_op
const exprt & case_op() const
Definition: std_code.h:1456
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
c_typecheck_baset::implicit_typecast_arithmetic
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecheck_typecast.cpp:50
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
typet::subtype
const typet & subtype() const
Definition: type.h:47
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1439
ansi_c_declaration.h
ANSI-CC Language Type Checking.
code_blockt::from_list
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:188
ansi_c_declarationt::declarators
const declaratorst & declarators() const
Definition: ansi_c_declaration.h:217
code_whilet
codet representing a while statement.
Definition: std_code.h:896
codet::op0
exprt & op0()
Definition: expr.h:102
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:45
c_typecheck_baset::typecheck_while
virtual void typecheck_while(code_whilet &code)
Definition: c_typecheck_code.cpp:731
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1669
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:209
irept::make_nil
void make_nil()
Definition: irep.h:475
typet
The type of an expression, extends irept.
Definition: type.h:29
c_typecheck_base.h
ANSI-C Language Type Checking.
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:774
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
code_gcc_switch_case_ranget::upper
const exprt & upper() const
upper bound of range
Definition: std_code.h:1535
c_typecheck_baset::typecheck_declaration
void typecheck_declaration(ansi_c_declarationt &)
Definition: c_typecheck_base.cpp:625
c_typecheck_baset::typecheck_break
virtual void typecheck_break(codet &code)
Definition: c_typecheck_code.cpp:206
c_typecheck_baset::to_string
virtual std::string to_string(const exprt &expr)
Definition: c_typecheck_base.cpp:24
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
exprt
Base class for all expressions.
Definition: expr.h:53
to_code_while
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:940
code_gcc_switch_case_ranget
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1513
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:764
messaget::eom
static eomt eom
Definition: message.h:297
c_typecheck_baset::typecheck_spec_expr
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:797
configt::ansi_c
struct configt::ansi_ct ansi_c
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void_type
empty_typet void_type()
Definition: c_types.cpp:253
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:746
code_labelt::code
codet & code()
Definition: std_code.h:1393
code_gcc_switch_case_ranget::lower
const exprt & lower() const
lower bound of range
Definition: std_code.h:1523
c_typecheck_baset::clean_code
std::list< codet > clean_code
Definition: c_typecheck_base.h:242
ansi_c_declaratort::get_name
irep_idt get_name() const
Definition: ansi_c_declaration.h:42
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:3552
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
to_code_switch_case
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1493
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
c_typecheck_baset::typecheck_continue
virtual void typecheck_continue(codet &code)
Definition: c_typecheck_code.cpp:216
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
c_typecheck_baset::typecheck_assigns
virtual void typecheck_assigns(const code_typet &function_declarator, const irept &spec)
Definition: c_typecheck_code.cpp:808
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:958
expr_initializer.h
Expression Initialization.
messaget::error
mstreamt & error() const
Definition: message.h:399
ansi_c_declaratort
Definition: ansi_c_declaration.h:21
empty_typet
The empty type.
Definition: std_types.h:46
code_switch_caset::is_default
bool is_default() const
Definition: std_code.h:1446
c_typecheck_baset::typecheck_asm
virtual void typecheck_asm(code_asmt &code)
Definition: c_typecheck_code.cpp:137
ansi_c_declaratort::get_base_name
irep_idt get_base_name() const
Definition: ansi_c_declaration.h:47
c_typecheck_baset::implicit_typecast_bool
virtual void implicit_typecast_bool(exprt &expr)
Definition: c_typecheck_base.h:117
code_gcc_switch_case_ranget::code
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1547
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
to_code_goto
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1161
c_typecheck_baset::typecheck_label
virtual void typecheck_label(code_labelt &code)
Definition: c_typecheck_code.cpp:476
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1127
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:816
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1375
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
c_typecheck_baset::case_is_allowed
bool case_is_allowed
Definition: c_typecheck_base.h:155
c_typecheck_baset::continue_is_allowed
bool continue_is_allowed
Definition: c_typecheck_base.h:154
c_typecheck_baset::is_complete_type
virtual bool is_complete_type(const typet &type) const
Definition: c_typecheck_code.cpp:342
ranget
A range is a pair of a begin and an end iterators.
Definition: range.h:396
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1420
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
c_typecheck_baset::typecheck_expression
virtual void typecheck_expression(codet &code)
Definition: c_typecheck_code.cpp:371
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:1002
c_typecheck_baset::typecheck_goto
virtual void typecheck_goto(code_gotot &code)
Definition: c_typecheck_code.cpp:545
c_typecheck_baset::typecheck_code
virtual void typecheck_code(codet &code)
Definition: c_typecheck_code.cpp:26
irept::swap
void swap(irept &irep)
Definition: irep.h:463
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:903
code_whilet::body
const codet & body() const
Definition: std_code.h:913
irept::is_nil
bool is_nil() const
Definition: irep.h:398
codet::op2
exprt & op2()
Definition: expr.h:108
irept::id
const irep_idt & id() const
Definition: irep.h:418
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1359
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
to_code_asm_gcc
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition: std_code.h:1789
to_ansi_c_declaration
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
Definition: ansi_c_declaration.h:264
c_typecheck_baset::typecheck_switch
virtual void typecheck_switch(codet &code)
Definition: c_typecheck_code.cpp:668
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
c_typecheck_baset::typecheck_return
virtual void typecheck_return(code_returnt &code)
Definition: c_typecheck_code.cpp:631
c_typecheck_baset::typecheck_dowhile
virtual void typecheck_dowhile(code_dowhilet &code)
Definition: c_typecheck_code.cpp:764
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
c_typecheck_baset::labels_used
std::map< irep_idt, source_locationt > labels_used
Definition: c_typecheck_base.h:160
c_typecheck_baset::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: c_typecheck_expr.cpp:41
config
configt config
Definition: config.cpp:24
c_typecheck_baset::switch_op_type
typet switch_op_type
Definition: c_typecheck_base.h:156
source_locationt
Definition: source_location.h:20
to_code_gcc_switch_case_range
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition: std_code.h:1577
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
c_typecheck_baset::break_is_allowed
bool break_is_allowed
Definition: c_typecheck_base.h:153
code_labelt::get_label
const irep_idt & get_label() const
Definition: std_code.h:1383
to_code_asm
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1698
c_typecheck_baset::typecheck_for
virtual void typecheck_for(codet &code)
Definition: c_typecheck_code.cpp:385
code_switcht::value
const exprt & value() const
Definition: std_code.h:841
code_returnt::has_return_value
bool has_return_value() const
Definition: std_code.h:1330
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
ansi_c_declarationt
Definition: ansi_c_declaration.h:73
c_typecheck_baset::typecheck_decl
virtual void typecheck_decl(codet &code)
Definition: c_typecheck_code.cpp:226
c_typecheck_baset::typecheck_gcc_switch_case_range
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &)
Definition: c_typecheck_code.cpp:520
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
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:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
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:160
code_switcht
codet representing a switch statement.
Definition: std_code.h:834
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
code_dowhilet::body
const codet & body() const
Definition: std_code.h:975
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
code_ifthenelset::else_case
const codet & else_case() const
Definition: std_code.h:784
c_typecheck_baset::typecheck_assign
virtual void typecheck_assign(codet &expr)
Definition: c_typecheck_code.cpp:171
to_code_switch
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:878
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:157
code_gotot::get_destination
const irep_idt & get_destination() const
Definition: std_code.h:1139
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
codet::op3
exprt & op3()
Definition: expr.h:111
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
code_switch_caset::code
codet & code()
Definition: std_code.h:1466
c_typecheck_baset::typecheck_start_thread
virtual void typecheck_start_thread(codet &code)
Definition: c_typecheck_code.cpp:619
config.h
code_dowhilet::cond
const exprt & cond() const
Definition: std_code.h:965
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:574
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
exprt::operands
operandst & operands()
Definition: expr.h:95
c_typecheck_baset::start_typecheck_code
virtual void start_typecheck_code()
Definition: c_typecheck_code.cpp:21
c_typecheck_baset::typecheck_switch_case
virtual void typecheck_switch_case(code_switch_caset &code)
Definition: c_typecheck_code.cpp:484
codet::op1
exprt & op1()
Definition: expr.h:105
c_typecheck_baset::typecheck_gcc_computed_goto
virtual void typecheck_gcc_computed_goto(codet &code)
Definition: c_typecheck_code.cpp:551
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_asmt::get_flavor
const irep_idt & get_flavor() const
Definition: std_code.h:1679
code_switcht::body
const codet & body() const
Definition: std_code.h:851
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1320
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
messaget::warning
mstreamt & warning() const
Definition: message.h:404
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:127
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h
c_typecheck_baset::typecheck_gcc_local_label
virtual void typecheck_gcc_local_label(codet &code)
Definition: c_typecheck_code.cpp:539
code_blockt::end_location
source_locationt end_location() const
Definition: std_code.h:227
c_typecheck_baset::typecheck_block
virtual void typecheck_block(code_blockt &code)
Definition: c_typecheck_code.cpp:187
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:35