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 #include <util/string_constant.h>
19 
20 #include "ansi_c_declaration.h"
21 
23 {
25 }
26 
28 {
29  if(code.id()!=ID_code)
30  {
32  error() << "expected code, got " << code.pretty() << eom;
33  throw 0;
34  }
35 
36  code.type() = empty_typet();
37 
38  const irep_idt &statement=code.get_statement();
39 
40  if(statement==ID_expression)
42  else if(statement==ID_label)
44  else if(statement==ID_switch_case)
46  else if(statement==ID_gcc_switch_case_range)
48  else if(statement==ID_block)
50  else if(statement==ID_decl_block)
51  {
52  }
53  else if(statement==ID_ifthenelse)
55  else if(statement==ID_while)
57  else if(statement==ID_dowhile)
59  else if(statement==ID_for)
60  typecheck_for(code);
61  else if(statement==ID_switch)
62  typecheck_switch(code);
63  else if(statement==ID_break)
64  typecheck_break(code);
65  else if(statement==ID_goto)
67  else if(statement==ID_gcc_computed_goto)
69  else if(statement==ID_continue)
70  typecheck_continue(code);
71  else if(statement==ID_return)
73  else if(statement==ID_decl)
74  typecheck_decl(code);
75  else if(statement==ID_assign)
76  typecheck_assign(code);
77  else if(statement==ID_skip)
78  {
79  }
80  else if(statement==ID_asm)
82  else if(statement==ID_start_thread)
84  else if(statement==ID_gcc_local_label)
86  else if(statement==ID_msc_try_finally)
87  {
88  assert(code.operands().size()==2);
89  typecheck_code(to_code(code.op0()));
90  typecheck_code(to_code(code.op1()));
91  }
92  else if(statement==ID_msc_try_except)
93  {
94  assert(code.operands().size()==3);
95  typecheck_code(to_code(code.op0()));
96  typecheck_expr(code.op1());
97  typecheck_code(to_code(code.op2()));
98  }
99  else if(statement==ID_msc_leave)
100  {
101  // fine as is, but should check that we
102  // are in a 'try' block
103  }
104  else if(statement==ID_static_assert)
105  {
106  PRECONDITION(code.operands().size() == 2);
107 
108  typecheck_expr(code.op0());
109  typecheck_expr(code.op1());
110 
111  implicit_typecast_bool(code.op0());
112  make_constant(code.op0());
113 
114  if(code.op0().is_false())
115  {
116  // failed
118  error() << "static assertion failed";
119  if(code.op1().id() == ID_string_constant)
120  error() << ": " << to_string_constant(code.op1()).get_value();
121  error() << eom;
122  throw 0;
123  }
124  }
125  else if(statement==ID_CPROVER_try_catch ||
126  statement==ID_CPROVER_try_finally)
127  {
128  assert(code.operands().size()==2);
129  typecheck_code(to_code(code.op0()));
130  typecheck_code(to_code(code.op1()));
131  }
132  else if(statement==ID_CPROVER_throw)
133  {
134  assert(code.operands().empty());
135  }
136  else if(statement==ID_assume ||
137  statement==ID_assert)
138  {
139  // These are not generated by the C/C++ parsers,
140  // but we allow them for the benefit of other users
141  // of the typechecker.
142  assert(code.operands().size()==1);
143  typecheck_expr(code.op0());
144  }
145  else
146  {
148  error() << "unexpected statement: " << statement << eom;
149  throw 0;
150  }
151 }
152 
154 {
155  const irep_idt flavor = code.get_flavor();
156 
157  if(flavor==ID_gcc)
158  {
159  // These have 5 operands.
160  // The first operand is a string.
161  // Operands 1, 2, 3, 4 are lists of expressions.
162 
163  // Operand 1: OutputOperands
164  // Operand 2: InputOperands
165  // Operand 3: Clobbers
166  // Operand 4: GotoLabels
167 
168  auto &code_asm_gcc = to_code_asm_gcc(code);
169 
170  typecheck_expr(code_asm_gcc.asm_text());
171 
172  // the operands are lists of expressions
173  for(auto &op : ranget<exprt::operandst::iterator>(
174  code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
175  {
176  for(auto &expr : op.operands())
177  typecheck_expr(expr);
178  }
179  }
180  else if(flavor==ID_msc)
181  {
182  assert(code.operands().size()==1);
183  typecheck_expr(code.op0());
184  }
185 }
186 
188 {
189  if(code.operands().size()!=2)
190  {
192  error() << "assignment statement expected to have two operands"
193  << eom;
194  throw 0;
195  }
196 
197  typecheck_expr(code.op0());
198  typecheck_expr(code.op1());
199 
200  implicit_typecast(code.op1(), code.op0().type());
201 }
202 
204 {
205  for(auto &c : code.statements())
206  typecheck_code(c);
207 
208  // do decl-blocks
209 
210  code_blockt new_ops;
211  new_ops.statements().reserve(code.statements().size());
212 
213  for(auto &code_op : code.statements())
214  {
215  if(code_op.is_not_nil())
216  new_ops.add(std::move(code_op));
217  }
218 
219  code.statements().swap(new_ops.statements());
220 }
221 
223 {
224  if(!break_is_allowed)
225  {
227  error() << "break not allowed here" << eom;
228  throw 0;
229  }
230 }
231 
233 {
235  {
237  error() << "continue not allowed here" << eom;
238  throw 0;
239  }
240 }
241 
243 {
244  // this comes with 1 operand, which is a declaration
245  if(code.operands().size()!=1)
246  {
248  error() << "decl expected to have 1 operand" << eom;
249  throw 0;
250  }
251 
252  // op0 must be declaration
253  if(code.op0().id()!=ID_declaration)
254  {
256  error() << "decl statement expected to have declaration as operand"
257  << eom;
258  throw 0;
259  }
260 
261  ansi_c_declarationt declaration;
262  declaration.swap(code.op0());
263 
264  if(declaration.get_is_static_assert())
265  {
266  codet new_code(ID_static_assert);
267  new_code.add_source_location()=code.source_location();
268  new_code.operands().swap(declaration.operands());
269  code.swap(new_code);
270  typecheck_code(code);
271  return; // done
272  }
273 
274  typecheck_declaration(declaration);
275 
276  std::list<codet> new_code;
277 
278  // iterate over declarators
279 
280  for(const auto &d : declaration.declarators())
281  {
282  irep_idt identifier = d.get_name();
283 
284  // look it up
285  symbol_tablet::symbolst::const_iterator s_it=
286  symbol_table.symbols.find(identifier);
287 
288  if(s_it==symbol_table.symbols.end())
289  {
291  error() << "failed to find decl symbol '" << identifier
292  << "' in symbol table" << eom;
293  throw 0;
294  }
295 
296  const symbolt &symbol=s_it->second;
297 
298  // This must not be an incomplete type, unless it's 'extern'
299  // or a typedef.
300  if(!symbol.is_type &&
301  !symbol.is_extern &&
302  !is_complete_type(symbol.type))
303  {
304  error().source_location=symbol.location;
305  error() << "incomplete type not permitted here" << eom;
306  throw 0;
307  }
308 
309  // see if it's a typedef
310  // or a function
311  // or static
312  if(symbol.is_type ||
313  symbol.type.id()==ID_code ||
314  symbol.is_static_lifetime)
315  {
316  // we ignore
317  }
318  else
319  {
320  code_declt decl(symbol.symbol_expr());
321  decl.add_source_location() = symbol.location;
322  decl.symbol().add_source_location() = symbol.location;
323 
324  // add initializer, if any
325  if(symbol.value.is_not_nil())
326  {
327  decl.operands().resize(2);
328  decl.op1() = symbol.value;
329  }
330 
331  new_code.push_back(decl);
332  }
333  }
334 
335  // stash away any side-effects in the declaration
336  new_code.splice(new_code.begin(), clean_code);
337 
338  if(new_code.empty())
339  {
340  source_locationt source_location=code.source_location();
341  code=code_skipt();
342  code.add_source_location()=source_location;
343  }
344  else if(new_code.size()==1)
345  {
346  code.swap(new_code.front());
347  }
348  else
349  {
350  // build a decl-block
351  auto code_block=code_blockt::from_list(new_code);
352  code_block.set_statement(ID_decl_block);
353  code.swap(code_block);
354  }
355 }
356 
358 {
359  if(type.id() == ID_array)
360  {
361  if(to_array_type(type).size().is_nil())
362  return false;
363  return is_complete_type(type.subtype());
364  }
365  else if(type.id()==ID_struct || type.id()==ID_union)
366  {
367  const auto &struct_union_type = to_struct_union_type(type);
368 
369  if(struct_union_type.is_incomplete())
370  return false;
371 
372  for(const auto &c : struct_union_type.components())
373  if(!is_complete_type(c.type()))
374  return false;
375  }
376  else if(type.id()==ID_vector)
377  return is_complete_type(type.subtype());
378  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
379  {
380  return is_complete_type(follow(type));
381  }
382 
383  return true;
384 }
385 
387 {
388  if(code.operands().size()!=1)
389  {
391  error() << "expression statement expected to have one operand"
392  << eom;
393  throw 0;
394  }
395 
396  exprt &op=code.op0();
397  typecheck_expr(op);
398 }
399 
401 {
402  if(code.operands().size()!=4)
403  {
405  error() << "for expected to have four operands" << eom;
406  throw 0;
407  }
408 
409  // the "for" statement has an implicit block around it,
410  // since code.op0() may contain declarations
411  //
412  // we therefore transform
413  //
414  // for(a;b;c) d;
415  //
416  // to
417  //
418  // { a; for(;b;c) d; }
419  //
420  // if config.ansi_c.for_has_scope
421 
423  code.op0().is_nil())
424  {
425  if(code.op0().is_not_nil())
426  typecheck_code(to_code(code.op0()));
427 
428  if(code.op1().is_nil())
429  code.op1()=true_exprt();
430  else
431  {
432  typecheck_expr(code.op1());
433  implicit_typecast_bool(code.op1());
434  }
435 
436  if(code.op2().is_not_nil())
437  typecheck_expr(code.op2());
438 
439  if(code.op3().is_not_nil())
440  {
441  // save & set flags
442  bool old_break_is_allowed=break_is_allowed;
443  bool old_continue_is_allowed=continue_is_allowed;
444 
446 
447  // recursive call
448  if(to_code(code.op3()).get_statement()==ID_decl_block)
449  {
450  code_blockt code_block;
451  code_block.add_source_location()=code.op3().source_location();
452 
453  code_block.add(std::move(to_code(code.op3())));
454  code.op3().swap(code_block);
455  }
456  typecheck_code(to_code(code.op3()));
457 
458  // restore flags
459  break_is_allowed=old_break_is_allowed;
460  continue_is_allowed=old_continue_is_allowed;
461  }
462  }
463  else
464  {
465  code_blockt code_block;
466  code_block.add_source_location()=code.source_location();
467  if(to_code(code.op3()).get_statement()==ID_block)
468  {
469  code_block.set(
470  ID_C_end_location,
472  }
473  else
474  {
475  code_block.set(
476  ID_C_end_location,
477  code.op3().source_location());
478  }
479 
480  code_block.reserve_operands(2);
481  code_block.add(std::move(to_code(code.op0())));
482  code.op0().make_nil();
483  code_block.add(std::move(code));
484  code.swap(code_block);
485  typecheck_code(code); // recursive call
486  }
487 
488  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
489 }
490 
492 {
493  // record the label
495 
496  typecheck_code(code.code());
497 }
498 
500 {
501  if(code.operands().size()!=2)
502  {
504  error() << "switch_case expected to have two operands" << eom;
505  throw 0;
506  }
507 
508  typecheck_code(code.code());
509 
510  if(code.is_default())
511  {
512  if(!case_is_allowed)
513  {
515  error() << "did not expect default label here" << eom;
516  throw 0;
517  }
518  }
519  else
520  {
521  if(!case_is_allowed)
522  {
524  error() << "did not expect `case' here" << eom;
525  throw 0;
526  }
527 
528  exprt &case_expr=code.case_op();
529  typecheck_expr(case_expr);
530  implicit_typecast(case_expr, switch_op_type);
531  make_constant(case_expr);
532  }
533 }
534 
537 {
538  if(!case_is_allowed)
539  {
541  error() << "did not expect `case' here" << eom;
542  throw 0;
543  }
544 
545  typecheck_expr(code.lower());
546  typecheck_expr(code.upper());
549  make_constant(code.lower());
550  make_constant(code.upper());
551  typecheck_code(code.code());
552 }
553 
555 {
556  // these are just declarations, e.g.,
557  // __label__ here, there;
558 }
559 
561 {
562  // we record the label used
564 }
565 
567 {
568  if(code.operands().size()!=1)
569  {
571  error() << "computed-goto expected to have one operand" << eom;
572  throw 0;
573  }
574 
575  exprt &dest=code.op0();
576 
577  if(dest.id()!=ID_dereference)
578  {
580  error() << "computed-goto expected to have dereferencing operand"
581  << eom;
582  throw 0;
583  }
584 
585  typecheck_expr(to_unary_expr(dest).op());
586  dest.type() = void_type();
587 }
588 
590 {
591  if(code.operands().size()!=3)
592  {
594  error() << "ifthenelse expected to have three operands" << eom;
595  throw 0;
596  }
597 
598  exprt &cond=code.cond();
599 
600  typecheck_expr(cond);
601 
602  #if 0
603  if(cond.id()==ID_sideeffect &&
604  cond.get(ID_statement)==ID_assign)
605  {
606  warning("warning: assignment in if condition");
607  }
608  #endif
609 
611 
612  if(code.then_case().get_statement() == ID_decl_block)
613  {
614  code_blockt code_block({code.then_case()});
615  code_block.add_source_location()=code.then_case().source_location();
616  code.then_case() = code_block;
617  }
618 
619  typecheck_code(code.then_case());
620 
621  if(!code.else_case().is_nil())
622  {
623  if(code.else_case().get_statement() == ID_decl_block)
624  {
625  code_blockt code_block({code.else_case()});
626  code_block.add_source_location()=code.else_case().source_location();
627  code.else_case() = code_block;
628  }
629 
630  typecheck_code(code.else_case());
631  }
632 }
633 
635 {
636  if(code.operands().size()!=1)
637  {
639  error() << "start_thread expected to have one operand" << eom;
640  throw 0;
641  }
642 
643  typecheck_code(to_code(code.op0()));
644 }
645 
647 {
648  if(code.has_return_value())
649  {
651 
652  if(return_type.id() == ID_empty)
653  {
654  // gcc doesn't actually complain, it just warns!
655  if(code.return_value().type().id() != ID_empty)
656  {
658 
659  warning() << "function has return void ";
660  warning() << "but a return statement returning ";
661  warning() << to_string(code.return_value().type());
662  warning() << eom;
663 
665  }
666  }
667  else
669  }
670  else if(
671  return_type.id() != ID_empty && 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.return_value() =
680  }
681 }
682 
684 {
685  // we expect a code_switcht, but might return either a code_switcht or a
686  // code_blockt, hence don't use code_switcht in the interface
687  code_switcht &code_switch = to_code_switch(code);
688 
689  typecheck_expr(code_switch.value());
690 
691  // this needs to be promoted
692  implicit_typecast_arithmetic(code_switch.value());
693 
694  // save & set flags
695 
696  bool old_case_is_allowed(case_is_allowed);
697  bool old_break_is_allowed(break_is_allowed);
698  typet old_switch_op_type(switch_op_type);
699 
700  switch_op_type = code_switch.value().type();
702 
703  typecheck_code(code_switch.body());
704 
705  if(code_switch.body().get_statement() == ID_block)
706  {
707  // Collect all declarations before the first case, if there is any case
708  // (including a default one).
709  code_blockt wrapping_block;
710 
711  code_blockt &body_block = to_code_block(code_switch.body());
712  for(auto &statement : body_block.statements())
713  {
714  if(statement.get_statement() == ID_switch_case)
715  break;
716  else if(statement.get_statement() == ID_decl)
717  {
718  if(statement.operands().size() == 1)
719  {
720  wrapping_block.add(code_skipt());
721  wrapping_block.statements().back().swap(statement);
722  }
723  else
724  {
725  PRECONDITION(statement.operands().size() == 2);
726  wrapping_block.add(statement);
727  wrapping_block.statements().back().operands().pop_back();
728  statement.set_statement(ID_assign);
729  }
730  }
731  }
732 
733  if(!wrapping_block.statements().empty())
734  {
735  wrapping_block.add(std::move(code));
736  code.swap(wrapping_block);
737  }
738  }
739 
740  // restore flags
741  case_is_allowed=old_case_is_allowed;
742  break_is_allowed=old_break_is_allowed;
743  switch_op_type=old_switch_op_type;
744 }
745 
747 {
748  if(code.operands().size()!=2)
749  {
751  error() << "while expected to have two operands" << eom;
752  throw 0;
753  }
754 
755  typecheck_expr(code.cond());
757 
758  // save & set flags
759  bool old_break_is_allowed(break_is_allowed);
760  bool old_continue_is_allowed(continue_is_allowed);
761 
763 
764  if(code.body().get_statement()==ID_decl_block)
765  {
766  code_blockt code_block({code.body()});
767  code_block.add_source_location()=code.body().source_location();
768  code.body() = code_block;
769  }
770  typecheck_code(code.body());
771 
772  // restore flags
773  break_is_allowed=old_break_is_allowed;
774  continue_is_allowed=old_continue_is_allowed;
775 
776  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
777 }
778 
780 {
781  if(code.operands().size()!=2)
782  {
784  error() << "do while expected to have two operands" << eom;
785  throw 0;
786  }
787 
788  typecheck_expr(code.cond());
790 
791  // save & set flags
792  bool old_break_is_allowed(break_is_allowed);
793  bool old_continue_is_allowed(continue_is_allowed);
794 
796 
797  if(code.body().get_statement()==ID_decl_block)
798  {
799  code_blockt code_block({code.body()});
800  code_block.add_source_location()=code.body().source_location();
801  code.body() = code_block;
802  }
803  typecheck_code(code.body());
804 
805  // restore flags
806  break_is_allowed=old_break_is_allowed;
807  continue_is_allowed=old_continue_is_allowed;
808 
809  typecheck_spec_expr(code, ID_C_spec_loop_invariant);
810 }
811 
813 {
814  if(code.find(spec).is_not_nil())
815  {
816  exprt &constraint = static_cast<exprt &>(code.add(spec));
817 
818  typecheck_expr(constraint);
819  implicit_typecast_bool(constraint);
820  }
821 }
822 
824  const code_typet &function_declarator,
825  const irept &contract)
826 {
827  exprt assigns = static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
828 
829  // Make sure there is an assigns clause to check
830  if(assigns.is_not_nil())
831  {
832  for(const auto &curr_param : function_declarator.parameters())
833  {
834  if(curr_param.id() == ID_declaration)
835  {
836  const ansi_c_declarationt &param_declaration =
837  to_ansi_c_declaration(curr_param);
838 
839  for(const auto &decl : param_declaration.declarators())
840  {
841  typecheck_assigns(decl, assigns);
842  }
843  }
844  }
845  }
846 }
847 
849  const ansi_c_declaratort &declarator,
850  const exprt &assigns)
851 {
852  for(exprt curr_op : assigns.operands())
853  {
854  if(curr_op.id() != ID_symbol)
855  {
856  continue;
857  }
858  const symbol_exprt &symbol_op = to_symbol_expr(curr_op);
859 
860  if(symbol_op.get(ID_C_base_name) == declarator.get_base_name())
861  {
862  error().source_location = declarator.source_location();
863  error() << "Formal parameter " << declarator.get_name() << " without "
864  << "dereference appears in ASSIGNS clause. Assigning this "
865  << "parameter will never affect the state of the calling context."
866  << " Did you mean to write *" << declarator.get_name() << "?"
867  << eom;
868  throw 0;
869  }
870  }
871 }
872 
874  codet &code,
875  const irep_idt &spec)
876 {
877  if(code.find(spec).is_not_nil())
878  {
879  exprt &constraint = static_cast<exprt &>(code.add(spec));
880 
881  typecheck_expr(constraint);
882  }
883 }
c_typecheck_baset::typecheck_assigns_exprs
virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec)
Definition: c_typecheck_code.cpp:873
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:1488
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:329
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:1471
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:215
code_whilet
codet representing a while statement.
Definition: std_code.h:928
codet::op0
exprt & op0()
Definition: expr.h:103
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:125
c_typecheck_baset::typecheck_while
virtual void typecheck_while(code_whilet &code)
Definition: c_typecheck_code.cpp:746
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1701
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:464
typet
The type of an expression, extends irept.
Definition: type.h:28
c_typecheck_base.h
ANSI-C Language Type Checking.
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:806
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
code_gcc_switch_case_ranget::upper
const exprt & upper() const
upper bound of range
Definition: std_code.h:1567
c_typecheck_baset::typecheck_declaration
void typecheck_declaration(ansi_c_declarationt &)
Definition: c_typecheck_base.cpp:626
c_typecheck_baset::typecheck_break
virtual void typecheck_break(codet &code)
Definition: c_typecheck_code.cpp:222
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
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
to_code_while
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:972
code_gcc_switch_case_ranget
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1545
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:796
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:812
configt::ansi_c
struct configt::ansi_ct ansi_c
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
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:177
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:778
code_labelt::code
codet & code()
Definition: std_code.h:1425
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
code_gcc_switch_case_ranget::lower
const exprt & lower() const
lower bound of range
Definition: std_code.h:1555
c_typecheck_baset::clean_code
std::list< codet > clean_code
Definition: c_typecheck_base.h:243
ansi_c_declaratort::get_name
irep_idt get_name() const
Definition: ansi_c_declaration.h:40
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:3769
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:1525
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
c_typecheck_baset::typecheck_continue
virtual void typecheck_continue(codet &code)
Definition: c_typecheck_code.cpp:232
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
c_typecheck_baset::typecheck_assigns
virtual void typecheck_assigns(const code_typet &function_declarator, const irept &spec)
Definition: c_typecheck_code.cpp:823
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:990
expr_initializer.h
Expression Initialization.
messaget::error
mstreamt & error() const
Definition: message.h:399
ansi_c_declaratort
Definition: ansi_c_declaration.h:19
empty_typet
The empty type.
Definition: std_types.h:46
code_switch_caset::is_default
bool is_default() const
Definition: std_code.h:1478
c_typecheck_baset::typecheck_asm
virtual void typecheck_asm(code_asmt &code)
Definition: c_typecheck_code.cpp:153
ansi_c_declaratort::get_base_name
irep_idt get_base_name() const
Definition: ansi_c_declaration.h:45
c_typecheck_baset::implicit_typecast_bool
virtual void implicit_typecast_bool(exprt &expr)
Definition: c_typecheck_base.h:118
code_gcc_switch_case_ranget::code
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1579
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:1193
c_typecheck_baset::typecheck_label
virtual void typecheck_label(code_labelt &code)
Definition: c_typecheck_code.cpp:491
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1159
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:848
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
c_typecheck_baset::case_is_allowed
bool case_is_allowed
Definition: c_typecheck_base.h:156
c_typecheck_baset::continue_is_allowed
bool continue_is_allowed
Definition: c_typecheck_base.h:155
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:179
c_typecheck_baset::is_complete_type
virtual bool is_complete_type(const typet &type) const
Definition: c_typecheck_code.cpp:357
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:1452
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:386
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:68
to_code_dowhile
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:1034
c_typecheck_baset::typecheck_goto
virtual void typecheck_goto(code_gotot &code)
Definition: c_typecheck_code.cpp:560
c_typecheck_baset::typecheck_code
virtual void typecheck_code(codet &code)
Definition: c_typecheck_code.cpp:27
irept::swap
void swap(irept &irep)
Definition: irep.h:452
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:935
code_whilet::body
const codet & body() const
Definition: std_code.h:945
irept::is_nil
bool is_nil() const
Definition: irep.h:387
codet::op2
exprt & op2()
Definition: expr.h:109
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:1391
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:1821
to_ansi_c_declaration
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
Definition: ansi_c_declaration.h:262
c_typecheck_baset::typecheck_switch
virtual void typecheck_switch(codet &code)
Definition: c_typecheck_code.cpp:683
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
c_typecheck_baset::typecheck_return
virtual void typecheck_return(code_returnt &code)
Definition: c_typecheck_code.cpp:646
c_typecheck_baset::typecheck_dowhile
virtual void typecheck_dowhile(code_dowhilet &code)
Definition: c_typecheck_code.cpp:779
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:161
c_typecheck_baset::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: c_typecheck_expr.cpp:43
config
configt config
Definition: config.cpp:24
c_typecheck_baset::switch_op_type
typet switch_op_type
Definition: c_typecheck_base.h:157
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:1609
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
c_typecheck_baset::break_is_allowed
bool break_is_allowed
Definition: c_typecheck_base.h:154
code_labelt::get_label
const irep_idt & get_label() const
Definition: std_code.h:1415
to_code_asm
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1730
c_typecheck_baset::typecheck_for
virtual void typecheck_for(codet &code)
Definition: c_typecheck_code.cpp:400
code_switcht::value
const exprt & value() const
Definition: std_code.h:873
code_returnt::has_return_value
bool has_return_value() const
Definition: std_code.h:1362
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
ansi_c_declarationt
Definition: ansi_c_declaration.h:71
c_typecheck_baset::typecheck_decl
virtual void typecheck_decl(codet &code)
Definition: c_typecheck_code.cpp:242
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:535
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:1342
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:161
code_switcht
codet representing a switch statement.
Definition: std_code.h:866
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
code_dowhilet::body
const codet & body() const
Definition: std_code.h:1007
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:816
c_typecheck_baset::typecheck_assign
virtual void typecheck_assign(codet &expr)
Definition: c_typecheck_code.cpp:187
to_code_switch
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:910
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:158
code_gotot::get_destination
const irep_idt & get_destination() const
Definition: std_code.h:1171
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
codet::op3
exprt & op3()
Definition: expr.h:112
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
code_switch_caset::code
codet & code()
Definition: std_code.h:1498
c_typecheck_baset::typecheck_start_thread
virtual void typecheck_start_thread(codet &code)
Definition: c_typecheck_code.cpp:634
config.h
code_dowhilet::cond
const exprt & cond() const
Definition: std_code.h:997
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:589
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:383
exprt::operands
operandst & operands()
Definition: expr.h:96
c_typecheck_baset::start_typecheck_code
virtual void start_typecheck_code()
Definition: c_typecheck_code.cpp:22
c_typecheck_baset::typecheck_switch_case
virtual void typecheck_switch_case(code_switch_caset &code)
Definition: c_typecheck_code.cpp:499
codet::op1
exprt & op1()
Definition: expr.h:106
c_typecheck_baset::typecheck_gcc_computed_goto
virtual void typecheck_gcc_computed_goto(codet &code)
Definition: c_typecheck_code.cpp:566
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
code_asmt::get_flavor
const irep_idt & get_flavor() const
Definition: std_code.h:1711
code_switcht::body
const codet & body() const
Definition: std_code.h:883
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1352
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
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:128
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
c_types.h
c_typecheck_baset::typecheck_gcc_local_label
virtual void typecheck_gcc_local_label(codet &code)
Definition: c_typecheck_code.cpp:554
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:22
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:203
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