CBMC
Loading...
Searching...
No Matches
c_typecheck_code.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include <util/c_types.h>
13#include <util/config.h>
14#include <util/cprover_prefix.h>
15#include <util/expr_util.h>
16#include <util/range.h>
19
20#include "ansi_c_declaration.h"
21#include "c_expr.h"
22#include "c_typecheck_base.h"
23
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)
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 PRECONDITION(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 PRECONDITION(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 // C23 allows static_assert without message
109 PRECONDITION(code.operands().size() == 1 || code.operands().size() == 2);
110
111 typecheck_expr(code.op0());
112
113 if(code.operands().size() == 2)
114 typecheck_expr(code.op1());
115
117 make_constant(code.op0());
118
119 if(code.op0().is_false())
120 {
121 // failed
123 error() << "static assertion failed";
124 if(code.operands().size() == 2 && code.op1().id() == ID_string_constant)
125 error() << ": " << to_string_constant(code.op1()).value();
126 error() << eom;
127 throw 0;
128 }
129 }
130 else if(statement==ID_CPROVER_try_catch ||
131 statement==ID_CPROVER_try_finally)
132 {
133 PRECONDITION(code.operands().size() == 2);
134 typecheck_code(to_code(code.op0()));
135 typecheck_code(to_code(code.op1()));
136 }
137 else if(statement==ID_CPROVER_throw)
138 {
139 PRECONDITION(code.operands().empty());
140 }
141 else if(statement==ID_assume ||
142 statement==ID_assert)
143 {
144 // These are not generated by the C/C++ parsers,
145 // but we allow them for the benefit of other users
146 // of the typechecker.
147 PRECONDITION(code.operands().size() == 1);
148 typecheck_expr(code.op0());
149 }
150 else
151 {
153 error() << "unexpected statement: " << statement << eom;
154 throw 0;
155 }
156}
157
159{
160 const irep_idt flavor = code.get_flavor();
161
162 if(flavor==ID_gcc)
163 {
164 // These have 5 operands.
165 // The first operand is a string.
166 // Operands 1, 2, 3, 4 are lists of expressions.
167
168 // Operand 1: OutputOperands
169 // Operand 2: InputOperands
170 // Operand 3: Clobbers
171 // Operand 4: GotoLabels
172
173 auto &code_asm_gcc = to_code_asm_gcc(code);
174
175 typecheck_expr(code_asm_gcc.asm_text());
176
177 // the operands are lists of expressions
179 code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
180 {
181 for(auto &expr : op.operands())
182 typecheck_expr(expr);
183 }
184 }
185 else if(flavor==ID_msc)
186 {
187 PRECONDITION(code.operands().size() == 1);
188 typecheck_expr(code.op0());
189 }
190}
191
193{
194 if(code.operands().size()!=2)
195 {
197 error() << "assignment statement expected to have two operands"
198 << eom;
199 throw 0;
200 }
201
202 typecheck_expr(code.op0());
203 typecheck_expr(code.op1());
204
205 implicit_typecast(code.op1(), code.op0().type());
206}
207
209{
210 for(auto &c : code.statements())
212
213 // do decl-blocks
214
216 new_ops.statements().reserve(code.statements().size());
217
218 for(auto &code_op : code.statements())
219 {
220 if(code_op.is_not_nil())
221 new_ops.add(std::move(code_op));
222 }
223
224 code.statements().swap(new_ops.statements());
225}
226
228{
230 {
232 error() << "break not allowed here" << eom;
233 throw 0;
234 }
235}
236
238{
240 {
242 error() << "continue not allowed here" << eom;
243 throw 0;
244 }
245}
246
248{
249 // this comes with 1 operand, which is a declaration
250 if(code.operands().size()!=1)
251 {
253 error() << "decl expected to have 1 operand" << eom;
254 throw 0;
255 }
256
257 // op0 must be declaration
258 if(code.op0().id()!=ID_declaration)
259 {
261 error() << "decl statement expected to have declaration as operand"
262 << eom;
263 throw 0;
264 }
265
266 ansi_c_declarationt declaration;
267 declaration.swap(code.op0());
268
269 if(declaration.get_is_static_assert())
270 {
271 codet new_code(ID_static_assert);
272 new_code.add_source_location()=code.source_location();
273 new_code.operands().swap(declaration.operands());
274 code.swap(new_code);
275 typecheck_code(code);
276 return; // done
277 }
278
279 typecheck_declaration(declaration);
280
281 std::list<codet> new_code;
282
283 // iterate over declarators
284
285 for(const auto &d : declaration.declarators())
286 {
287 irep_idt identifier = d.get_name();
288
289 // look it up
290 symbol_table_baset::symbolst::const_iterator s_it =
291 symbol_table.symbols.find(identifier);
292
293 if(s_it==symbol_table.symbols.end())
294 {
296 error() << "failed to find decl symbol '" << identifier
297 << "' in symbol table" << eom;
298 throw 0;
299 }
300
301 const symbolt &symbol=s_it->second;
302
303 // This must not be an incomplete type, unless it's 'extern'
304 // or a typedef.
305 if(!symbol.is_type &&
306 !symbol.is_extern &&
307 !is_complete_type(symbol.type))
308 {
310 error() << "incomplete type not permitted here" << eom;
311 throw 0;
312 }
313
314 // see if it's a typedef
315 // or a function
316 // or static
317 if(symbol.is_type || symbol.type.id() == ID_code)
318 {
319 // we ignore
320 }
321 else if(symbol.is_static_lifetime)
322 {
323 // make sure the initialization value is a compile-time constant
324 if(symbol.value.is_not_nil())
325 {
326 exprt init_value = symbol.value;
328 }
329 }
330 else
331 {
332 code_frontend_declt decl(symbol.symbol_expr());
333 decl.add_source_location() = symbol.location;
334 decl.symbol().add_source_location() = symbol.location;
335
336 // add initializer, if any
337 if(symbol.value.is_not_nil())
338 {
339 decl.operands().resize(2);
340 decl.op1() = symbol.value;
341 }
342
343 new_code.push_back(decl);
344 }
345 }
346
347 // stash away any side-effects in the declaration
348 new_code.splice(new_code.begin(), clean_code);
349
350 if(new_code.empty())
351 {
352 source_locationt source_location=code.source_location();
353 code=code_skipt();
354 code.add_source_location()=source_location;
355 }
356 else if(new_code.size()==1)
357 {
358 code.swap(new_code.front());
359 }
360 else
361 {
362 // build a decl-block
363 auto code_block=code_blockt::from_list(new_code);
364 code_block.set_statement(ID_decl_block);
365 code.swap(code_block);
366 }
367}
368
370{
371 if(type.id() == ID_array)
372 {
373 const auto &array_type = to_array_type(type);
374
375 if(array_type.size().is_nil())
376 return false;
377
378 return is_complete_type(array_type.element_type());
379 }
380 else if(type.id()==ID_struct || type.id()==ID_union)
381 {
382 const auto &struct_union_type = to_struct_union_type(type);
383
384 if(struct_union_type.is_incomplete())
385 return false;
386
387 for(const auto &c : struct_union_type.components())
388 if(!is_complete_type(c.type()))
389 return false;
390 }
391 else if(type.id()==ID_vector)
392 return is_complete_type(to_vector_type(type).element_type());
394 {
396 }
398 {
400 }
401
402 return true;
403}
404
406{
407 if(code.operands().size()!=1)
408 {
410 error() << "expression statement expected to have one operand"
411 << eom;
412 throw 0;
413 }
414
415 exprt &op=code.op0();
416 typecheck_expr(op);
417}
418
420{
421 if(code.operands().size()!=4)
422 {
424 error() << "for expected to have four operands" << eom;
425 throw 0;
426 }
427
428 // the "for" statement has an implicit block around it,
429 // since code.op0() may contain declarations
430 //
431 // we therefore transform
432 //
433 // for(a;b;c) d;
434 //
435 // to
436 //
437 // { a; for(;b;c) d; }
438 //
439 // if config.ansi_c.for_has_scope
440
441 if(!config.ansi_c.for_has_scope ||
442 code.op0().is_nil())
443 {
444 if(code.op0().is_not_nil())
445 typecheck_code(to_code(code.op0()));
446
447 if(code.op1().is_nil())
448 code.op1()=true_exprt();
449 else
450 {
451 typecheck_expr(code.op1());
453 }
454
455 if(code.op2().is_not_nil())
456 typecheck_expr(code.op2());
457
458 if(code.op3().is_not_nil())
459 {
460 // save & set flags
463
465
466 // recursive call
467 if(to_code(code.op3()).get_statement()==ID_decl_block)
468 {
470 code_block.add_source_location()=code.op3().source_location();
471
472 code_block.add(std::move(to_code(code.op3())));
473 code.op3().swap(code_block);
474 }
475 typecheck_code(to_code(code.op3()));
476
477 // restore flags
480 }
481 }
482 else
483 {
485 code_block.add_source_location()=code.source_location();
486 if(to_code(code.op3()).get_statement()==ID_block)
487 {
488 code_block.set(
490 to_code_block(to_code(code.op3())).end_location());
491 }
492 else
493 {
494 code_block.set(
496 code.op3().source_location());
497 }
498
499 code_block.reserve_operands(2);
500 code_block.add(std::move(to_code(code.op0())));
501 code.op0().make_nil();
502 code_block.add(std::move(code));
503 code.swap(code_block);
504 typecheck_code(code); // recursive call
505 }
506
509
510 if(code.find(ID_C_spec_assigns).is_not_nil())
511 {
513 static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
514 }
515
516 if(code.find(ID_C_spec_frees).is_not_nil())
517 {
519 static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
520 }
521}
522
524{
525 // record the label
526 if(!labels_defined.emplace(code.get_label(), code.source_location()).second)
527 {
529 error() << "duplicate label '" << code.get_label() << "'" << eom;
530 throw 0;
531 }
532
533 typecheck_code(code.code());
534}
535
537{
538 if(code.operands().size()!=2)
539 {
541 error() << "switch_case expected to have two operands" << eom;
542 throw 0;
543 }
544
545 typecheck_code(code.code());
546
547 if(code.is_default())
548 {
549 if(!case_is_allowed)
550 {
552 error() << "did not expect default label here" << eom;
553 throw 0;
554 }
555 }
556 else
557 {
558 if(!case_is_allowed)
559 {
561 error() << "did not expect `case' here" << eom;
562 throw 0;
563 }
564
565 exprt &case_expr=code.case_op();
569 }
570}
571
574{
575 if(!case_is_allowed)
576 {
578 error() << "did not expect `case' here" << eom;
579 throw 0;
580 }
581
582 typecheck_expr(code.lower());
583 typecheck_expr(code.upper());
586 make_constant(code.lower());
587 make_constant(code.upper());
588 typecheck_code(code.code());
589}
590
592{
593 // these are just declarations, e.g.,
594 // __label__ here, there;
595}
596
598{
599 // we record the label used
601}
602
604{
605 if(code.operands().size()!=1)
606 {
608 error() << "computed-goto expected to have one operand" << eom;
609 throw 0;
610 }
611
612 exprt &dest=code.op0();
613
614 if(dest.id()!=ID_dereference)
615 {
617 error() << "computed-goto expected to have dereferencing operand"
618 << eom;
619 throw 0;
620 }
621
622 typecheck_expr(to_unary_expr(dest).op());
623 dest.type() = void_type();
624}
625
627{
628 if(code.operands().size()!=3)
629 {
631 error() << "ifthenelse expected to have three operands" << eom;
632 throw 0;
633 }
634
635 exprt &cond=code.cond();
636
637 typecheck_expr(cond);
638
640
641 if(code.then_case().get_statement() == ID_decl_block)
642 {
644 code_block.add_source_location()=code.then_case().source_location();
645 code.then_case() = code_block;
646 }
647
649
650 if(!code.else_case().is_nil())
651 {
652 if(code.else_case().get_statement() == ID_decl_block)
653 {
655 code_block.add_source_location()=code.else_case().source_location();
656 code.else_case() = code_block;
657 }
658
660 }
661}
662
664{
665 if(code.operands().size()!=1)
666 {
668 error() << "start_thread expected to have one operand" << eom;
669 throw 0;
670 }
671
672 typecheck_code(to_code(code.op0()));
673}
674
676{
677 if(code.has_return_value())
678 {
680
681 if(return_type.id() == ID_empty)
682 {
683 // gcc doesn't actually complain, it just warns!
684 if(code.return_value().type().id() != ID_empty)
685 {
687
688 warning() << "function has return void ";
689 warning() << "but a return statement returning ";
690 warning() << to_string(code.return_value().type());
691 warning() << eom;
692
694 }
695 }
696 else
698 }
699 else if(
702 {
703 // gcc doesn't actually complain, it just warns!
705 warning() << "non-void function should return a value" << eom;
706
707 code.return_value() =
709 }
710}
711
713{
714 // we expect a code_switcht, but might return either a code_switcht or a
715 // code_blockt, hence don't use code_switcht in the interface
717
719
720 // this needs to be promoted
722
723 // save & set flags
724
728
729 switch_op_type = code_switch.value().type();
731
733
734 if(code_switch.body().get_statement() == ID_block)
735 {
736 // Collect all declarations before the first case, if there is any case
737 // (including a default one).
739
741 for(auto &statement : body_block.statements())
742 {
743 if(statement.get_statement() == ID_switch_case)
744 break;
745 else if(statement.get_statement() == ID_decl)
746 {
747 if(statement.operands().size() == 1)
748 {
750 wrapping_block.statements().back().swap(statement);
751 }
752 else
753 {
754 PRECONDITION(statement.operands().size() == 2);
755 wrapping_block.add(statement);
756 wrapping_block.statements().back().operands().pop_back();
757 statement.set_statement(ID_assign);
758 }
759 }
760 }
761
762 if(!wrapping_block.statements().empty())
763 {
764 wrapping_block.add(std::move(code));
765 code.swap(wrapping_block);
766 }
767 }
768
769 // restore flags
773}
774
776{
777 if(code.operands().size()!=2)
778 {
780 error() << "while expected to have two operands" << eom;
781 throw 0;
782 }
783
784 typecheck_expr(code.cond());
786
787 // save & set flags
790
792
793 if(code.body().get_statement()==ID_decl_block)
794 {
795 code_blockt code_block({code.body()});
796 code_block.add_source_location()=code.body().source_location();
797 code.body() = code_block;
798 }
799 typecheck_code(code.body());
800
801 // restore flags
804
807
808 if(code.find(ID_C_spec_assigns).is_not_nil())
809 {
811 static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
812 }
813
814 if(code.find(ID_C_spec_frees).is_not_nil())
815 {
817 static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
818 }
819}
820
822{
823 if(code.operands().size()!=2)
824 {
826 error() << "do while expected to have two operands" << eom;
827 throw 0;
828 }
829
830 typecheck_expr(code.cond());
832
833 // save & set flags
836
838
839 if(code.body().get_statement()==ID_decl_block)
840 {
841 code_blockt code_block({code.body()});
842 code_block.add_source_location()=code.body().source_location();
843 code.body() = code_block;
844 }
845 typecheck_code(code.body());
846
847 // restore flags
850
853
854 if(code.find(ID_C_spec_assigns).is_not_nil())
855 {
857 static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
858 }
859
860 if(code.find(ID_C_spec_frees).is_not_nil())
861 {
863 static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
864 }
865}
866
868{
869 if(has_subexpr(expr, ID_side_effect))
870 {
872 "side-effects not allowed in assigns clause targets",
873 expr.source_location()};
874 }
875 if(has_subexpr(expr, ID_if))
876 {
878 "ternary expressions not allowed in assigns clause targets",
879 expr.source_location()};
880 }
881}
882
884{
885 // compute type
886 typecheck_expr(condition);
887
888 // make it boolean if needed
889 implicit_typecast_bool(condition);
890
891 // non-fatal warnings
893 {
894 // Remark: we allow function calls without further checks for now because
895 // they are mandatory for some applications.
896 // The next step must be to check that the called functions have a contract
897 // with an empty assigns clause and that they indeed satisfy their contract
898 // using a CI check.
900 warning()
901 << "function with possible side-effect called in target's condition"
902 << eom;
903 }
904
905 if(condition.type().id() == ID_empty)
906 {
908 "void-typed expressions not allowed as assigns clause conditions",
909 condition.source_location()};
910 }
911
912 if(has_subexpr(condition, [&](const exprt &subexpr) {
915 }))
916 {
918 "side-effects not allowed in assigns clause conditions",
919 condition.source_location()};
920 }
921
922 if(has_subexpr(condition, ID_if))
923 {
925 "ternary expressions not allowed in assigns clause conditions",
926 condition.source_location()};
927 }
928}
929
931 exprt::operandst &targets,
932 const std::function<void(exprt &)> typecheck_target,
933 const std::string &clause_type)
934{
936
937 for(auto &target : targets)
938 {
940 {
942 "expected a conditional target group expression in " + clause_type +
943 "clause, found " + id2string(target.id()),
944 target.source_location()};
945 }
946
949
950 // typecheck condition
951 auto &condition = conditional_target_group.condition();
952 typecheck_spec_condition(condition);
953
954 if(condition.is_true())
955 {
956 // if the condition is trivially true,
957 // simplify expr and expose the bare expressions
958 for(auto &actual_target : conditional_target_group.targets())
959 {
961 new_targets.push_back(actual_target);
962 }
963 }
964 else
965 {
966 // if the condition is not trivially true, typecheck in place
967 for(auto &actual_target : conditional_target_group.targets())
968 {
970 }
971 new_targets.push_back(std::move(target));
972 }
973 }
974
975 // now each target is either:
976 // - a simple side-effect-free unconditional lvalue expression or
977 // - a conditional target group expression with a non-trivial condition
978
979 // update original vector in-place
980 std::swap(targets, new_targets);
981}
982
984{
985 const std::function<void(exprt &)> typecheck_target = [&](exprt &target) {
987 };
989}
990
992{
993 const std::function<void(exprt &)> typecheck_target = [&](exprt &target) {
995 };
997}
998
1000{
1001 // compute type
1002 typecheck_expr(target);
1003
1004 if(target.get_bool(ID_C_lvalue))
1005 {
1006 if(target.type().id() == ID_empty)
1007 {
1009 "lvalue expressions with void type not allowed in assigns clauses",
1010 target.source_location()};
1011 }
1012 throw_on_side_effects(target);
1013 return;
1014 }
1016 {
1017 const auto &funcall = to_side_effect_expr_function_call(target);
1018 if(!can_cast_expr<symbol_exprt>(funcall.function()))
1019 {
1021 "function pointer calls not allowed in assigns clauses",
1022 target.source_location());
1023 }
1024
1025 if(target.type().id() != ID_empty)
1026 {
1028 "expecting void return type for function '" +
1029 id2string(to_symbol_expr(funcall.function()).get_identifier()) +
1030 "' called in assigns clause",
1031 target.source_location());
1032 }
1033
1034 for(const auto &argument : funcall.arguments())
1036 }
1037 else
1038 {
1039 // if we reach this point the target did not pass the checks
1041 "assigns clause target must be a non-void lvalue or a call to a function "
1042 "returning void",
1043 target.source_location());
1044 }
1045}
1046
1048{
1049 // compute type
1050 typecheck_expr(target);
1051 const auto &type = target.type();
1052
1054 {
1055 // an expression with pointer-type without side effects
1056 throw_on_side_effects(target);
1057 }
1059 {
1060 // A call to a void function symbol without other side effects
1061 const auto &funcall = to_side_effect_expr_function_call(target);
1062
1063 if(!can_cast_expr<symbol_exprt>(funcall.function()))
1064 {
1066 "function pointer calls not allowed in frees clauses",
1067 target.source_location());
1068 }
1069
1070 if(type.id() != ID_empty)
1071 {
1073 "expecting void return type for function '" +
1074 id2string(to_symbol_expr(funcall.function()).get_identifier()) +
1075 "' called in frees clause",
1076 target.source_location());
1077 }
1078
1079 for(const auto &argument : funcall.arguments())
1081 }
1082 else
1083 {
1084 // anything else is rejected
1086 "frees clause target must be a pointer-typed expression or a call to a "
1087 "function returning void",
1088 target.source_location());
1089 }
1090}
1091
1093{
1094 if(code.find(ID_C_spec_loop_invariant).is_not_nil())
1095 {
1096 for(auto &invariant :
1097 (static_cast<exprt &>(code.add(ID_C_spec_loop_invariant)).operands()))
1098 {
1099 typecheck_expr(invariant);
1100 implicit_typecast_bool(invariant);
1102 invariant,
1103 ID_old,
1104 CPROVER_PREFIX "old is not allowed in loop invariants.");
1105 }
1106 }
1107}
1108
1110{
1111 if(code.find(ID_C_spec_decreases).is_not_nil())
1112 {
1113 for(auto &decreases_clause_component :
1114 (static_cast<exprt &>(code.add(ID_C_spec_decreases)).operands()))
1115 {
1118 }
1119 }
1120}
ANSI-CC Language Type Checking.
configt config
Definition config.cpp:25
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:306
void validate_expr(const shuffle_vector_exprt &value)
Definition c_expr.h:82
ANSI-C Language Type Checking.
empty_typet void_type()
Definition c_types.cpp:245
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const declaratorst & declarators() const
bool get_is_static_assert() const
symbol_table_baset & symbol_table
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 throw_on_side_effects(const exprt &expr)
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)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_spec_frees_target(exprt &target)
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 typecheck_spec_condition(exprt &condition)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_conditional_targets(exprt::operandst &targets, const std::function< void(exprt &)> typecheck_target, const std::string &clause_type)
virtual void typecheck_for(codet &code)
virtual void typecheck_switch(codet &code)
virtual void typecheck_spec_frees(exprt::operandst &targets)
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
code_operandst & statements()
Definition std_code.h:138
codet representation of a do while statement.
Definition std_code.h:672
const codet & body() const
Definition std_code.h:689
const exprt & cond() const
Definition std_code.h:679
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
const exprt & upper() const
upper bound of range
Definition std_code.h:1119
const exprt & lower() const
lower bound of range
Definition std_code.h:1107
codet & code()
the statement to be executed when the case applies
Definition std_code.h:1131
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 exprt & cond() const
Definition std_code.h:478
const codet & else_case() const
Definition std_code.h:498
const codet & then_case() const
Definition std_code.h:488
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
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
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.
exprt & op3()
Definition expr.h:142
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
const irep_idt & get_statement() const
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:38
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
Thrown when we can't handle something in an input source file.
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
bool is_nil() const
Definition irep.h:368
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
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:74
bool is_static_lifetime
Definition symbol.h:70
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:3191
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
#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
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const code_switch_caset & to_code_switch_case(const codet &code)
Definition std_code.h:1077
const code_gotot & to_code_goto(const codet &code)
Definition std_code.h:875
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition std_code.h:1373
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition std_code.h:943
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
const code_dowhilet & to_code_dowhile(const codet &code)
Definition std_code.h:716
const code_whilet & to_code_while(const codet &code)
Definition std_code.h:654
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
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_ifthenelset & to_code_ifthenelse(const codet &code)
Definition std_code.h:530
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition std_code.h:1161
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition std_code.h:1498
code_asmt & to_code_asm(codet &code)
Definition std_code.h:1282
const code_switcht & to_code_switch(const codet &code)
Definition std_code.h:592
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:426
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
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)
Author: Diffblue Ltd.