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/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/config.h>
17 #include <util/expr_util.h>
18 #include <util/range.h>
19 #include <util/string_constant.h>
20 
21 #include "ansi_c_declaration.h"
22 #include "c_expr.h"
23 
25 {
27 }
28 
30 {
31  if(code.id()!=ID_code)
32  {
34  error() << "expected code, got " << code.pretty() << eom;
35  throw 0;
36  }
37 
38  code.type() = empty_typet();
39 
40  const irep_idt &statement=code.get_statement();
41 
42  if(statement==ID_expression)
44  else if(statement==ID_label)
46  else if(statement==ID_switch_case)
48  else if(statement==ID_gcc_switch_case_range)
50  else if(statement==ID_block)
52  else if(statement==ID_decl_block)
53  {
54  }
55  else if(statement==ID_ifthenelse)
57  else if(statement==ID_while)
59  else if(statement==ID_dowhile)
61  else if(statement==ID_for)
62  typecheck_for(code);
63  else if(statement==ID_switch)
64  typecheck_switch(code);
65  else if(statement==ID_break)
66  typecheck_break(code);
67  else if(statement==ID_goto)
69  else if(statement==ID_gcc_computed_goto)
71  else if(statement==ID_continue)
72  typecheck_continue(code);
73  else if(statement==ID_return)
75  else if(statement==ID_decl)
76  typecheck_decl(code);
77  else if(statement==ID_assign)
78  typecheck_assign(code);
79  else if(statement==ID_skip)
80  {
81  }
82  else if(statement==ID_asm)
84  else if(statement==ID_start_thread)
86  else if(statement==ID_gcc_local_label)
88  else if(statement==ID_msc_try_finally)
89  {
90  assert(code.operands().size()==2);
91  typecheck_code(to_code(code.op0()));
92  typecheck_code(to_code(code.op1()));
93  }
94  else if(statement==ID_msc_try_except)
95  {
96  assert(code.operands().size()==3);
97  typecheck_code(to_code(code.op0()));
98  typecheck_expr(code.op1());
99  typecheck_code(to_code(code.op2()));
100  }
101  else if(statement==ID_msc_leave)
102  {
103  // fine as is, but should check that we
104  // are in a 'try' block
105  }
106  else if(statement==ID_static_assert)
107  {
108  PRECONDITION(code.operands().size() == 2);
109 
110  typecheck_expr(code.op0());
111  typecheck_expr(code.op1());
112 
113  implicit_typecast_bool(code.op0());
114  make_constant(code.op0());
115 
116  if(code.op0().is_false())
117  {
118  // failed
120  error() << "static assertion failed";
121  if(code.op1().id() == ID_string_constant)
122  error() << ": " << to_string_constant(code.op1()).get_value();
123  error() << eom;
124  throw 0;
125  }
126  }
127  else if(statement==ID_CPROVER_try_catch ||
128  statement==ID_CPROVER_try_finally)
129  {
130  assert(code.operands().size()==2);
131  typecheck_code(to_code(code.op0()));
132  typecheck_code(to_code(code.op1()));
133  }
134  else if(statement==ID_CPROVER_throw)
135  {
136  assert(code.operands().empty());
137  }
138  else if(statement==ID_assume ||
139  statement==ID_assert)
140  {
141  // These are not generated by the C/C++ parsers,
142  // but we allow them for the benefit of other users
143  // of the typechecker.
144  assert(code.operands().size()==1);
145  typecheck_expr(code.op0());
146  }
147  else
148  {
150  error() << "unexpected statement: " << statement << eom;
151  throw 0;
152  }
153 }
154 
156 {
157  const irep_idt flavor = code.get_flavor();
158 
159  if(flavor==ID_gcc)
160  {
161  // These have 5 operands.
162  // The first operand is a string.
163  // Operands 1, 2, 3, 4 are lists of expressions.
164 
165  // Operand 1: OutputOperands
166  // Operand 2: InputOperands
167  // Operand 3: Clobbers
168  // Operand 4: GotoLabels
169 
170  auto &code_asm_gcc = to_code_asm_gcc(code);
171 
172  typecheck_expr(code_asm_gcc.asm_text());
173 
174  // the operands are lists of expressions
175  for(auto &op : ranget<exprt::operandst::iterator>(
176  code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
177  {
178  for(auto &expr : op.operands())
179  typecheck_expr(expr);
180  }
181  }
182  else if(flavor==ID_msc)
183  {
184  assert(code.operands().size()==1);
185  typecheck_expr(code.op0());
186  }
187 }
188 
190 {
191  if(code.operands().size()!=2)
192  {
194  error() << "assignment statement expected to have two operands"
195  << eom;
196  throw 0;
197  }
198 
199  typecheck_expr(code.op0());
200  typecheck_expr(code.op1());
201 
202  implicit_typecast(code.op1(), code.op0().type());
203 }
204 
206 {
207  for(auto &c : code.statements())
208  typecheck_code(c);
209 
210  // do decl-blocks
211 
212  code_blockt new_ops;
213  new_ops.statements().reserve(code.statements().size());
214 
215  for(auto &code_op : code.statements())
216  {
217  if(code_op.is_not_nil())
218  new_ops.add(std::move(code_op));
219  }
220 
221  code.statements().swap(new_ops.statements());
222 }
223 
225 {
226  if(!break_is_allowed)
227  {
229  error() << "break not allowed here" << eom;
230  throw 0;
231  }
232 }
233 
235 {
237  {
239  error() << "continue not allowed here" << eom;
240  throw 0;
241  }
242 }
243 
245 {
246  // this comes with 1 operand, which is a declaration
247  if(code.operands().size()!=1)
248  {
250  error() << "decl expected to have 1 operand" << eom;
251  throw 0;
252  }
253 
254  // op0 must be declaration
255  if(code.op0().id()!=ID_declaration)
256  {
258  error() << "decl statement expected to have declaration as operand"
259  << eom;
260  throw 0;
261  }
262 
263  ansi_c_declarationt declaration;
264  declaration.swap(code.op0());
265 
266  if(declaration.get_is_static_assert())
267  {
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(const auto &d : declaration.declarators())
283  {
284  irep_idt identifier = d.get_name();
285 
286  // look it up
287  symbol_tablet::symbolst::const_iterator s_it=
288  symbol_table.symbols.find(identifier);
289 
290  if(s_it==symbol_table.symbols.end())
291  {
293  error() << "failed to find decl symbol '" << identifier
294  << "' in symbol table" << eom;
295  throw 0;
296  }
297 
298  const symbolt &symbol=s_it->second;
299 
300  // This must not be an incomplete type, unless it's 'extern'
301  // or a typedef.
302  if(!symbol.is_type &&
303  !symbol.is_extern &&
304  !is_complete_type(symbol.type))
305  {
306  error().source_location=symbol.location;
307  error() << "incomplete type not permitted here" << eom;
308  throw 0;
309  }
310 
311  // see if it's a typedef
312  // or a function
313  // or static
314  if(symbol.is_type || symbol.type.id() == ID_code)
315  {
316  // we ignore
317  }
318  else if(symbol.is_static_lifetime)
319  {
320  // make sure the initialization value is a compile-time constant
321  if(symbol.value.is_not_nil())
322  {
323  exprt init_value = symbol.value;
324  make_constant(init_value);
325  }
326  }
327  else
328  {
329  code_frontend_declt decl(symbol.symbol_expr());
330  decl.add_source_location() = symbol.location;
331  decl.symbol().add_source_location() = symbol.location;
332 
333  // add initializer, if any
334  if(symbol.value.is_not_nil())
335  {
336  decl.operands().resize(2);
337  decl.op1() = symbol.value;
338  }
339 
340  new_code.push_back(decl);
341  }
342  }
343 
344  // stash away any side-effects in the declaration
345  new_code.splice(new_code.begin(), clean_code);
346 
347  if(new_code.empty())
348  {
349  source_locationt source_location=code.source_location();
350  code=code_skipt();
351  code.add_source_location()=source_location;
352  }
353  else if(new_code.size()==1)
354  {
355  code.swap(new_code.front());
356  }
357  else
358  {
359  // build a decl-block
360  auto code_block=code_blockt::from_list(new_code);
361  code_block.set_statement(ID_decl_block);
362  code.swap(code_block);
363  }
364 }
365 
367 {
368  if(type.id() == ID_array)
369  {
370  const auto &array_type = to_array_type(type);
371 
372  if(array_type.size().is_nil())
373  return false;
374 
375  return is_complete_type(array_type.element_type());
376  }
377  else if(type.id()==ID_struct || type.id()==ID_union)
378  {
379  const auto &struct_union_type = to_struct_union_type(type);
380 
381  if(struct_union_type.is_incomplete())
382  return false;
383 
384  for(const auto &c : struct_union_type.components())
385  if(!is_complete_type(c.type()))
386  return false;
387  }
388  else if(type.id()==ID_vector)
389  return is_complete_type(to_vector_type(type).element_type());
390  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
391  {
392  return is_complete_type(follow(type));
393  }
394 
395  return true;
396 }
397 
399 {
400  if(code.operands().size()!=1)
401  {
403  error() << "expression statement expected to have one operand"
404  << eom;
405  throw 0;
406  }
407 
408  exprt &op=code.op0();
409  typecheck_expr(op);
410 }
411 
413 {
414  if(code.operands().size()!=4)
415  {
417  error() << "for expected to have four operands" << eom;
418  throw 0;
419  }
420 
421  // the "for" statement has an implicit block around it,
422  // since code.op0() may contain declarations
423  //
424  // we therefore transform
425  //
426  // for(a;b;c) d;
427  //
428  // to
429  //
430  // { a; for(;b;c) d; }
431  //
432  // if config.ansi_c.for_has_scope
433 
435  code.op0().is_nil())
436  {
437  if(code.op0().is_not_nil())
438  typecheck_code(to_code(code.op0()));
439 
440  if(code.op1().is_nil())
441  code.op1()=true_exprt();
442  else
443  {
444  typecheck_expr(code.op1());
445  implicit_typecast_bool(code.op1());
446  }
447 
448  if(code.op2().is_not_nil())
449  typecheck_expr(code.op2());
450 
451  if(code.op3().is_not_nil())
452  {
453  // save & set flags
454  bool old_break_is_allowed=break_is_allowed;
455  bool old_continue_is_allowed=continue_is_allowed;
456 
458 
459  // recursive call
460  if(to_code(code.op3()).get_statement()==ID_decl_block)
461  {
462  code_blockt code_block;
463  code_block.add_source_location()=code.op3().source_location();
464 
465  code_block.add(std::move(to_code(code.op3())));
466  code.op3().swap(code_block);
467  }
468  typecheck_code(to_code(code.op3()));
469 
470  // restore flags
471  break_is_allowed=old_break_is_allowed;
472  continue_is_allowed=old_continue_is_allowed;
473  }
474  }
475  else
476  {
477  code_blockt code_block;
478  code_block.add_source_location()=code.source_location();
479  if(to_code(code.op3()).get_statement()==ID_block)
480  {
481  code_block.set(
482  ID_C_end_location,
484  }
485  else
486  {
487  code_block.set(
488  ID_C_end_location,
489  code.op3().source_location());
490  }
491 
492  code_block.reserve_operands(2);
493  code_block.add(std::move(to_code(code.op0())));
494  code.op0().make_nil();
495  code_block.add(std::move(code));
496  code.swap(code_block);
497  typecheck_code(code); // recursive call
498  }
499 
502 
503  if(code.find(ID_C_spec_assigns).is_not_nil())
504  {
506  static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
507  }
508 }
509 
511 {
512  // record the label
513  if(!labels_defined.emplace(code.get_label(), code.source_location()).second)
514  {
516  error() << "duplicate label '" << code.get_label() << "'" << eom;
517  throw 0;
518  }
519 
520  typecheck_code(code.code());
521 }
522 
524 {
525  if(code.operands().size()!=2)
526  {
528  error() << "switch_case expected to have two operands" << eom;
529  throw 0;
530  }
531 
532  typecheck_code(code.code());
533 
534  if(code.is_default())
535  {
536  if(!case_is_allowed)
537  {
539  error() << "did not expect default label here" << eom;
540  throw 0;
541  }
542  }
543  else
544  {
545  if(!case_is_allowed)
546  {
548  error() << "did not expect `case' here" << eom;
549  throw 0;
550  }
551 
552  exprt &case_expr=code.case_op();
553  typecheck_expr(case_expr);
554  implicit_typecast(case_expr, switch_op_type);
555  make_constant(case_expr);
556  }
557 }
558 
561 {
562  if(!case_is_allowed)
563  {
565  error() << "did not expect `case' here" << eom;
566  throw 0;
567  }
568 
569  typecheck_expr(code.lower());
570  typecheck_expr(code.upper());
573  make_constant(code.lower());
574  make_constant(code.upper());
575  typecheck_code(code.code());
576 }
577 
579 {
580  // these are just declarations, e.g.,
581  // __label__ here, there;
582 }
583 
585 {
586  // we record the label used
588 }
589 
591 {
592  if(code.operands().size()!=1)
593  {
595  error() << "computed-goto expected to have one operand" << eom;
596  throw 0;
597  }
598 
599  exprt &dest=code.op0();
600 
601  if(dest.id()!=ID_dereference)
602  {
604  error() << "computed-goto expected to have dereferencing operand"
605  << eom;
606  throw 0;
607  }
608 
609  typecheck_expr(to_unary_expr(dest).op());
610  dest.type() = void_type();
611 }
612 
614 {
615  if(code.operands().size()!=3)
616  {
618  error() << "ifthenelse expected to have three operands" << eom;
619  throw 0;
620  }
621 
622  exprt &cond=code.cond();
623 
624  typecheck_expr(cond);
625 
626  #if 0
627  if(cond.id()==ID_sideeffect &&
628  cond.get(ID_statement)==ID_assign)
629  {
630  warning("warning: assignment in if condition");
631  }
632  #endif
633 
635 
636  if(code.then_case().get_statement() == ID_decl_block)
637  {
638  code_blockt code_block({code.then_case()});
639  code_block.add_source_location()=code.then_case().source_location();
640  code.then_case() = code_block;
641  }
642 
643  typecheck_code(code.then_case());
644 
645  if(!code.else_case().is_nil())
646  {
647  if(code.else_case().get_statement() == ID_decl_block)
648  {
649  code_blockt code_block({code.else_case()});
650  code_block.add_source_location()=code.else_case().source_location();
651  code.else_case() = code_block;
652  }
653 
654  typecheck_code(code.else_case());
655  }
656 }
657 
659 {
660  if(code.operands().size()!=1)
661  {
663  error() << "start_thread expected to have one operand" << eom;
664  throw 0;
665  }
666 
667  typecheck_code(to_code(code.op0()));
668 }
669 
671 {
672  if(code.has_return_value())
673  {
675 
676  if(return_type.id() == ID_empty)
677  {
678  // gcc doesn't actually complain, it just warns!
679  if(code.return_value().type().id() != ID_empty)
680  {
682 
683  warning() << "function has return void ";
684  warning() << "but a return statement returning ";
685  warning() << to_string(code.return_value().type());
686  warning() << eom;
687 
689  }
690  }
691  else
693  }
694  else if(
695  return_type.id() != ID_empty && return_type.id() != ID_constructor &&
696  return_type.id() != ID_destructor)
697  {
698  // gcc doesn't actually complain, it just warns!
700  warning() << "non-void function should return a value" << eom;
701 
702  code.return_value() =
704  }
705 }
706 
708 {
709  // we expect a code_switcht, but might return either a code_switcht or a
710  // code_blockt, hence don't use code_switcht in the interface
711  code_switcht &code_switch = to_code_switch(code);
712 
713  typecheck_expr(code_switch.value());
714 
715  // this needs to be promoted
716  implicit_typecast_arithmetic(code_switch.value());
717 
718  // save & set flags
719 
720  bool old_case_is_allowed(case_is_allowed);
721  bool old_break_is_allowed(break_is_allowed);
722  typet old_switch_op_type(switch_op_type);
723 
724  switch_op_type = code_switch.value().type();
726 
727  typecheck_code(code_switch.body());
728 
729  if(code_switch.body().get_statement() == ID_block)
730  {
731  // Collect all declarations before the first case, if there is any case
732  // (including a default one).
733  code_blockt wrapping_block;
734 
735  code_blockt &body_block = to_code_block(code_switch.body());
736  for(auto &statement : body_block.statements())
737  {
738  if(statement.get_statement() == ID_switch_case)
739  break;
740  else if(statement.get_statement() == ID_decl)
741  {
742  if(statement.operands().size() == 1)
743  {
744  wrapping_block.add(code_skipt());
745  wrapping_block.statements().back().swap(statement);
746  }
747  else
748  {
749  PRECONDITION(statement.operands().size() == 2);
750  wrapping_block.add(statement);
751  wrapping_block.statements().back().operands().pop_back();
752  statement.set_statement(ID_assign);
753  }
754  }
755  }
756 
757  if(!wrapping_block.statements().empty())
758  {
759  wrapping_block.add(std::move(code));
760  code.swap(wrapping_block);
761  }
762  }
763 
764  // restore flags
765  case_is_allowed=old_case_is_allowed;
766  break_is_allowed=old_break_is_allowed;
767  switch_op_type=old_switch_op_type;
768 }
769 
771 {
772  if(code.operands().size()!=2)
773  {
775  error() << "while expected to have two operands" << eom;
776  throw 0;
777  }
778 
779  typecheck_expr(code.cond());
781 
782  // save & set flags
783  bool old_break_is_allowed(break_is_allowed);
784  bool old_continue_is_allowed(continue_is_allowed);
785 
787 
788  if(code.body().get_statement()==ID_decl_block)
789  {
790  code_blockt code_block({code.body()});
791  code_block.add_source_location()=code.body().source_location();
792  code.body() = code_block;
793  }
794  typecheck_code(code.body());
795 
796  // restore flags
797  break_is_allowed=old_break_is_allowed;
798  continue_is_allowed=old_continue_is_allowed;
799 
802 
803  if(code.find(ID_C_spec_assigns).is_not_nil())
804  {
806  static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
807  }
808 }
809 
811 {
812  if(code.operands().size()!=2)
813  {
815  error() << "do while expected to have two operands" << eom;
816  throw 0;
817  }
818 
819  typecheck_expr(code.cond());
821 
822  // save & set flags
823  bool old_break_is_allowed(break_is_allowed);
824  bool old_continue_is_allowed(continue_is_allowed);
825 
827 
828  if(code.body().get_statement()==ID_decl_block)
829  {
830  code_blockt code_block({code.body()});
831  code_block.add_source_location()=code.body().source_location();
832  code.body() = code_block;
833  }
834  typecheck_code(code.body());
835 
836  // restore flags
837  break_is_allowed=old_break_is_allowed;
838  continue_is_allowed=old_continue_is_allowed;
839 
842 
843  if(code.find(ID_C_spec_assigns).is_not_nil())
844  {
846  static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
847  }
848 }
849 
851 {
852  // compute type
853  typecheck_expr(condition);
854 
855  // make it boolean if needed
856  implicit_typecast_bool(condition);
857 
858  // non-fatal warnings
860  {
861  // Remark: we allow function calls without further checks for now because
862  // they are mandatory for some applications.
863  // The next step must be to check that the called functions have a contract
864  // with an empty assigns clause and that they indeed satisfy their contract
865  // using a CI check.
866  warning().source_location = condition.source_location();
867  warning()
868  << "function with possible side-effect called in target's condition"
869  << eom;
870  }
871 
872  // fatal errors
873  bool must_throw = false;
874 
875  if(condition.type().id() == ID_empty)
876  {
877  must_throw = true;
878  error().source_location = condition.source_location();
879  error() << "void-typed expressions not allowed as assigns clause conditions"
880  << eom;
881  }
882 
883  if(has_subexpr(condition, [&](const exprt &subexpr) {
884  return can_cast_expr<side_effect_exprt>(subexpr) &&
886  }))
887  {
888  must_throw = true;
889  error().source_location = condition.source_location();
890  error() << "side-effects not allowed in assigns clause conditions" << eom;
891  }
892 
893  if(has_subexpr(condition, ID_if))
894  {
895  must_throw = true;
896  error().source_location = condition.source_location();
897  error() << "ternary expressions not allowed in assigns "
898  "clause conditions"
899  << eom;
900  }
901 
902  if(must_throw)
903  throw 0;
904 }
905 
907 {
908  // compute type
909  typecheck_expr(target);
910 
911  // fatal errors
912  bool must_throw = false;
913  if(target.type().id() == ID_empty)
914  {
915  must_throw = true;
917  error() << "void-typed expressions not allowed as assigns clause targets"
918  << eom;
919  }
920 
921  if(!target.get_bool(ID_C_lvalue) && target.id() != ID_pointer_object)
922  {
923  must_throw = true;
925  error() << "assigns clause target must be an lvalue or " CPROVER_PREFIX
926  "POINTER_OBJECT expression"
927  << eom;
928  }
929 
930  // Remark: an expression can be an lvalue and still contain side effects
931  // or ternary expressions. We detect them in a second step.
932  if(has_subexpr(target, ID_side_effect))
933  {
934  must_throw = true;
936  error() << "side-effects not allowed in assigns clause targets" << eom;
937  }
938 
939  if(has_subexpr(target, ID_if))
940  {
941  must_throw = true;
943  error() << "ternary expressions not allowed in assigns "
944  "clause targets"
945  << eom;
946  }
947 
948  if(must_throw)
949  throw 0;
950 }
951 
953 {
954  exprt::operandst tmp;
955  bool must_throw = false;
956 
957  for(auto &target : targets)
958  {
960  {
961  must_throw = true;
962  error().source_location = target.source_location();
963  error() << "expected ID_conditional_target_group expression in assigns "
964  "clause, found "
965  << id2string(target.id()) << eom;
966  }
967 
968  auto &conditional_target_group = to_conditional_target_group_expr(target);
969  validate_expr(conditional_target_group);
970 
971  // typecheck condition
972  auto &condition = conditional_target_group.condition();
974 
975  if(condition.is_true())
976  {
977  // if the condition is trivially true,
978  // simplify expr and expose the bare expressions
979  for(auto &actual_target : conditional_target_group.targets())
980  {
981  typecheck_spec_assigns_target(actual_target);
982  tmp.push_back(actual_target);
983  }
984  }
985  else
986  {
987  // if the condition is not trivially true, typecheck in place
988  for(auto &actual_target : conditional_target_group.targets())
989  {
990  typecheck_spec_assigns_target(actual_target);
991  }
992  tmp.push_back(std::move(target));
993  }
994  }
995 
996  // at least one target was not as expected
997  if(must_throw)
998  throw 0;
999 
1000  // now each target is either:
1001  // - a simple side-effect-free unconditional lvalue expression or
1002  // - a conditional target group expression with a non-trivial condition
1003 
1004  // update original vector in-place
1005  std::swap(targets, tmp);
1006 }
1007 
1009 {
1010  if(code.find(ID_C_spec_loop_invariant).is_not_nil())
1011  {
1012  for(auto &invariant :
1013  (static_cast<exprt &>(code.add(ID_C_spec_loop_invariant)).operands()))
1014  {
1015  typecheck_expr(invariant);
1016  implicit_typecast_bool(invariant);
1018  invariant,
1019  ID_old,
1020  CPROVER_PREFIX "old is not allowed in loop invariants.");
1021  }
1022  }
1023 }
1024 
1026 {
1027  if(code.find(ID_C_spec_decreases).is_not_nil())
1028  {
1029  for(auto &decreases_clause_component :
1030  (static_cast<exprt &>(code.add(ID_C_spec_decreases)).operands()))
1031  {
1032  typecheck_expr(decreases_clause_component);
1033  implicit_typecast_arithmetic(decreases_clause_component);
1034  }
1035  }
1036 }
ANSI-CC Language Type Checking.
API to expression classes that are internal to the C frontend.
const conditional_target_group_exprt & to_conditional_target_group_expr(const exprt &expr)
Cast an exprt to a conditional_target_group_exprt.
Definition: c_expr.h:305
bool can_cast_expr< conditional_target_group_exprt >(const exprt &base)
Definition: c_expr.h:293
void validate_expr(const shuffle_vector_exprt &value)
Definition: c_expr.h:81
ANSI-C Language Type Checking.
empty_typet void_type()
Definition: c_types.cpp:263
const declaratorst & declarators() const
bool get_is_static_assert() const
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_break(codet &code)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr(exprt &expr)
virtual void typecheck_block(code_blockt &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_while(code_whilet &code)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
virtual void typecheck_spec_assigns_condition(exprt &condition)
virtual void typecheck_decl(codet &code)
virtual void typecheck_spec_decreases(codet &code)
virtual void make_constant(exprt &expr)
virtual void typecheck_assign(codet &expr)
virtual void typecheck_continue(codet &code)
symbol_tablet & symbol_table
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_spec_assigns_target(exprt &target)
virtual void typecheck_gcc_local_label(codet &code)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_for(codet &code)
virtual void typecheck_switch(codet &code)
virtual void typecheck_expression(codet &code)
virtual void typecheck_return(code_frontend_returnt &)
virtual void typecheck_spec_assigns(exprt::operandst &targets)
virtual bool is_complete_type(const typet &type) const
virtual void typecheck_start_thread(codet &code)
virtual void typecheck_switch_case(code_switch_caset &code)
virtual void typecheck_spec_loop_invariant(codet &code)
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &)
virtual void implicit_typecast_bool(exprt &expr)
virtual void typecheck_dowhile(code_dowhilet &code)
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_label(code_labelt &code)
std::map< irep_idt, source_locationt > labels_defined
codet representation of an inline assembler statement.
Definition: std_code.h:1253
const irep_idt & get_flavor() const
Definition: std_code.h:1263
A codet representing sequential composition of program statements.
Definition: std_code.h:130
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:148
source_locationt end_location() const
Definition: std_code.h:187
void add(const codet &code)
Definition: std_code.h:168
code_operandst & statements()
Definition: std_code.h:138
codet representation of a do while statement.
Definition: std_code.h:672
const exprt & cond() const
Definition: std_code.h:679
const codet & body() const
Definition: std_code.h:689
A codet representing the declaration of a local variable.
Definition: std_code.h:347
symbol_exprt & symbol()
Definition: std_code.h:354
codet representation of a "return from a function" statement.
Definition: std_code.h:893
const exprt & return_value() const
Definition: std_code.h:903
bool has_return_value() const
Definition: std_code.h:913
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1097
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1131
const exprt & lower() const
lower bound of range
Definition: std_code.h:1107
const exprt & upper() const
upper bound of range
Definition: std_code.h:1119
codet representation of a goto statement.
Definition: std_code.h:841
const irep_idt & get_destination() const
Definition: std_code.h:853
codet representation of an if-then-else statement.
Definition: std_code.h:460
const codet & then_case() const
Definition: std_code.h:488
const exprt & cond() const
Definition: std_code.h:478
const codet & else_case() const
Definition: std_code.h:498
codet representation of a label for branch targets.
Definition: std_code.h:959
const irep_idt & get_label() const
Definition: std_code.h:967
codet & code()
Definition: std_code.h:977
A codet representing a skip statement.
Definition: std_code.h:322
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1023
codet & code()
Definition: std_code.h:1050
const exprt & case_op() const
Definition: std_code.h:1040
bool is_default() const
Definition: std_code.h:1030
codet representing a switch statement.
Definition: std_code.h:548
const exprt & value() const
Definition: std_code.h:555
const codet & body() const
Definition: std_code.h:565
codet representing a while statement.
Definition: std_code.h:610
const exprt & cond() const
Definition: std_code.h:617
const codet & body() const
Definition: std_code.h:627
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op3()
Definition: expr.h:108
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
void reserve_operands(operandst::size_type n)
Definition: expr.h:124
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
const irep_idt & get_value() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
bool is_extern
Definition: symbol.h:66
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:530
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:875
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:654
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1077
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1004
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:716
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:592
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:1730
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition: std_code.h:943
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition: std_code.h:1498
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition: std_code.h:1161
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition: std_code.h:1373
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1282
const codet & to_code(const exprt &expr)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const string_constantt & to_string_constant(const exprt &expr)
bool for_has_scope
Definition: config.h:123
A range is a pair of a begin and an end iterators.
Definition: range.h:396