cprover
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 PRECONDITION(code.operands().size() == 2);
109
110 typecheck_expr(code.op0());
111 typecheck_expr(code.op1());
112
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 PRECONDITION(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 PRECONDITION(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 PRECONDITION(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
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 PRECONDITION(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())
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{
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_table_baset::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 {
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)
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());
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 if(code.find(ID_C_spec_frees).is_not_nil())
510 {
512 static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
513 }
514}
515
517{
518 // record the label
519 if(!labels_defined.emplace(code.get_label(), code.source_location()).second)
520 {
522 error() << "duplicate label '" << code.get_label() << "'" << eom;
523 throw 0;
524 }
525
526 typecheck_code(code.code());
527}
528
530{
531 if(code.operands().size()!=2)
532 {
534 error() << "switch_case expected to have two operands" << eom;
535 throw 0;
536 }
537
538 typecheck_code(code.code());
539
540 if(code.is_default())
541 {
542 if(!case_is_allowed)
543 {
545 error() << "did not expect default label here" << eom;
546 throw 0;
547 }
548 }
549 else
550 {
551 if(!case_is_allowed)
552 {
554 error() << "did not expect `case' here" << eom;
555 throw 0;
556 }
557
558 exprt &case_expr=code.case_op();
559 typecheck_expr(case_expr);
561 make_constant(case_expr);
562 }
563}
564
567{
568 if(!case_is_allowed)
569 {
571 error() << "did not expect `case' here" << eom;
572 throw 0;
573 }
574
575 typecheck_expr(code.lower());
576 typecheck_expr(code.upper());
579 make_constant(code.lower());
580 make_constant(code.upper());
581 typecheck_code(code.code());
582}
583
585{
586 // these are just declarations, e.g.,
587 // __label__ here, there;
588}
589
591{
592 // we record the label used
594}
595
597{
598 if(code.operands().size()!=1)
599 {
601 error() << "computed-goto expected to have one operand" << eom;
602 throw 0;
603 }
604
605 exprt &dest=code.op0();
606
607 if(dest.id()!=ID_dereference)
608 {
610 error() << "computed-goto expected to have dereferencing operand"
611 << eom;
612 throw 0;
613 }
614
615 typecheck_expr(to_unary_expr(dest).op());
616 dest.type() = void_type();
617}
618
620{
621 if(code.operands().size()!=3)
622 {
624 error() << "ifthenelse expected to have three operands" << eom;
625 throw 0;
626 }
627
628 exprt &cond=code.cond();
629
630 typecheck_expr(cond);
631
632 #if 0
633 if(cond.id()==ID_sideeffect &&
634 cond.get(ID_statement)==ID_assign)
635 {
636 warning("warning: assignment in if condition");
637 }
638 #endif
639
641
642 if(code.then_case().get_statement() == ID_decl_block)
643 {
644 code_blockt code_block({code.then_case()});
645 code_block.add_source_location()=code.then_case().source_location();
646 code.then_case() = code_block;
647 }
648
650
651 if(!code.else_case().is_nil())
652 {
653 if(code.else_case().get_statement() == ID_decl_block)
654 {
655 code_blockt code_block({code.else_case()});
656 code_block.add_source_location()=code.else_case().source_location();
657 code.else_case() = code_block;
658 }
659
661 }
662}
663
665{
666 if(code.operands().size()!=1)
667 {
669 error() << "start_thread expected to have one operand" << eom;
670 throw 0;
671 }
672
673 typecheck_code(to_code(code.op0()));
674}
675
677{
678 if(code.has_return_value())
679 {
681
682 if(return_type.id() == ID_empty)
683 {
684 // gcc doesn't actually complain, it just warns!
685 if(code.return_value().type().id() != ID_empty)
686 {
688
689 warning() << "function has return void ";
690 warning() << "but a return statement returning ";
691 warning() << to_string(code.return_value().type());
692 warning() << eom;
693
695 }
696 }
697 else
699 }
700 else if(
701 return_type.id() != ID_empty && return_type.id() != ID_constructor &&
702 return_type.id() != ID_destructor)
703 {
704 // gcc doesn't actually complain, it just warns!
706 warning() << "non-void function should return a value" << eom;
707
708 code.return_value() =
710 }
711}
712
714{
715 // we expect a code_switcht, but might return either a code_switcht or a
716 // code_blockt, hence don't use code_switcht in the interface
717 code_switcht &code_switch = to_code_switch(code);
718
719 typecheck_expr(code_switch.value());
720
721 // this needs to be promoted
722 implicit_typecast_arithmetic(code_switch.value());
723
724 // save & set flags
725
726 bool old_case_is_allowed(case_is_allowed);
727 bool old_break_is_allowed(break_is_allowed);
728 typet old_switch_op_type(switch_op_type);
729
730 switch_op_type = code_switch.value().type();
732
733 typecheck_code(code_switch.body());
734
735 if(code_switch.body().get_statement() == ID_block)
736 {
737 // Collect all declarations before the first case, if there is any case
738 // (including a default one).
739 code_blockt wrapping_block;
740
741 code_blockt &body_block = to_code_block(code_switch.body());
742 for(auto &statement : body_block.statements())
743 {
744 if(statement.get_statement() == ID_switch_case)
745 break;
746 else if(statement.get_statement() == ID_decl)
747 {
748 if(statement.operands().size() == 1)
749 {
750 wrapping_block.add(code_skipt());
751 wrapping_block.statements().back().swap(statement);
752 }
753 else
754 {
755 PRECONDITION(statement.operands().size() == 2);
756 wrapping_block.add(statement);
757 wrapping_block.statements().back().operands().pop_back();
758 statement.set_statement(ID_assign);
759 }
760 }
761 }
762
763 if(!wrapping_block.statements().empty())
764 {
765 wrapping_block.add(std::move(code));
766 code.swap(wrapping_block);
767 }
768 }
769
770 // restore flags
771 case_is_allowed=old_case_is_allowed;
772 break_is_allowed=old_break_is_allowed;
773 switch_op_type=old_switch_op_type;
774}
775
777{
778 if(code.operands().size()!=2)
779 {
781 error() << "while expected to have two operands" << eom;
782 throw 0;
783 }
784
785 typecheck_expr(code.cond());
787
788 // save & set flags
789 bool old_break_is_allowed(break_is_allowed);
790 bool old_continue_is_allowed(continue_is_allowed);
791
793
794 if(code.body().get_statement()==ID_decl_block)
795 {
796 code_blockt code_block({code.body()});
797 code_block.add_source_location()=code.body().source_location();
798 code.body() = code_block;
799 }
800 typecheck_code(code.body());
801
802 // restore flags
803 break_is_allowed=old_break_is_allowed;
804 continue_is_allowed=old_continue_is_allowed;
805
808
809 if(code.find(ID_C_spec_assigns).is_not_nil())
810 {
812 static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
813 }
814
815 if(code.find(ID_C_spec_frees).is_not_nil())
816 {
818 static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
819 }
820}
821
823{
824 if(code.operands().size()!=2)
825 {
827 error() << "do while expected to have two operands" << eom;
828 throw 0;
829 }
830
831 typecheck_expr(code.cond());
833
834 // save & set flags
835 bool old_break_is_allowed(break_is_allowed);
836 bool old_continue_is_allowed(continue_is_allowed);
837
839
840 if(code.body().get_statement()==ID_decl_block)
841 {
842 code_blockt code_block({code.body()});
843 code_block.add_source_location()=code.body().source_location();
844 code.body() = code_block;
845 }
846 typecheck_code(code.body());
847
848 // restore flags
849 break_is_allowed=old_break_is_allowed;
850 continue_is_allowed=old_continue_is_allowed;
851
854
855 if(code.find(ID_C_spec_assigns).is_not_nil())
856 {
858 static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
859 }
860
861 if(code.find(ID_C_spec_frees).is_not_nil())
862 {
864 static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
865 }
866}
867
869{
870 if(has_subexpr(expr, ID_side_effect))
871 {
873 "side-effects not allowed in assigns clause targets",
874 expr.source_location()};
875 }
876 if(has_subexpr(expr, ID_if))
877 {
879 "ternary expressions not allowed in assigns clause targets",
880 expr.source_location()};
881 }
882}
883
885{
886 // compute type
887 typecheck_expr(condition);
888
889 // make it boolean if needed
890 implicit_typecast_bool(condition);
891
892 // non-fatal warnings
894 {
895 // Remark: we allow function calls without further checks for now because
896 // they are mandatory for some applications.
897 // The next step must be to check that the called functions have a contract
898 // with an empty assigns clause and that they indeed satisfy their contract
899 // using a CI check.
901 warning()
902 << "function with possible side-effect called in target's condition"
903 << eom;
904 }
905
906 if(condition.type().id() == ID_empty)
907 {
909 "void-typed expressions not allowed as assigns clause conditions",
910 condition.source_location()};
911 }
912
913 if(has_subexpr(condition, [&](const exprt &subexpr) {
914 return can_cast_expr<side_effect_exprt>(subexpr) &&
916 }))
917 {
919 "side-effects not allowed in assigns clause conditions",
920 condition.source_location()};
921 }
922
923 if(has_subexpr(condition, ID_if))
924 {
926 "ternary expressions not allowed in assigns clause conditions",
927 condition.source_location()};
928 }
929}
930
932 exprt::operandst &targets,
933 const std::function<void(exprt &)> typecheck_target,
934 const std::string &clause_type)
935{
936 exprt::operandst new_targets;
937
938 for(auto &target : targets)
939 {
941 {
943 "expected a conditional target group expression in " + clause_type +
944 "clause, found " + id2string(target.id()),
945 target.source_location()};
946 }
947
948 auto &conditional_target_group = to_conditional_target_group_expr(target);
949 validate_expr(conditional_target_group);
950
951 // typecheck condition
952 auto &condition = conditional_target_group.condition();
953 typecheck_spec_condition(condition);
954
955 if(condition.is_true())
956 {
957 // if the condition is trivially true,
958 // simplify expr and expose the bare expressions
959 for(auto &actual_target : conditional_target_group.targets())
960 {
961 typecheck_target(actual_target);
962 new_targets.push_back(actual_target);
963 }
964 }
965 else
966 {
967 // if the condition is not trivially true, typecheck in place
968 for(auto &actual_target : conditional_target_group.targets())
969 {
970 typecheck_target(actual_target);
971 }
972 new_targets.push_back(std::move(target));
973 }
974 }
975
976 // now each target is either:
977 // - a simple side-effect-free unconditional lvalue expression or
978 // - a conditional target group expression with a non-trivial condition
979
980 // update original vector in-place
981 std::swap(targets, new_targets);
982}
983
985{
986 const std::function<void(exprt &)> typecheck_target = [&](exprt &target) {
988 };
989 typecheck_conditional_targets(targets, typecheck_target, "assigns");
990}
991
993{
994 const std::function<void(exprt &)> typecheck_target = [&](exprt &target) {
996 };
997 typecheck_conditional_targets(targets, typecheck_target, "frees");
998}
999
1001{
1002 // compute type
1003 typecheck_expr(target);
1004
1005 if(target.get_bool(ID_C_lvalue))
1006 {
1007 if(target.type().id() == ID_empty)
1008 {
1010 "lvalue expressions with void type not allowed in assigns clauses",
1011 target.source_location()};
1012 }
1013 throw_on_side_effects(target);
1014 return;
1015 }
1017 {
1018 const auto &funcall = to_side_effect_expr_function_call(target);
1019 if(!can_cast_expr<symbol_exprt>(funcall.function()))
1020 {
1022 "function pointer calls not allowed in assigns clauses",
1023 target.source_location());
1024 }
1025
1026 if(target.type().id() != ID_empty)
1027 {
1029 "expecting void return type for function '" +
1030 id2string(to_symbol_expr(funcall.function()).get_identifier()) +
1031 "' called in assigns clause",
1032 target.source_location());
1033 }
1034
1035 for(const auto &argument : funcall.arguments())
1036 throw_on_side_effects(argument);
1037 }
1038 else
1039 {
1040 // if we reach this point the target did not pass the checks
1042 "assigns clause target must be a non-void lvalue or a call to a function "
1043 "returning void",
1044 target.source_location());
1045 }
1046}
1047
1049{
1050 // compute type
1051 typecheck_expr(target);
1052 const auto &type = target.type();
1053
1055 {
1056 // an expression with pointer-type without side effects
1057 throw_on_side_effects(target);
1058 }
1060 {
1061 // A call to a void function symbol without other side effects
1062 const auto &funcall = to_side_effect_expr_function_call(target);
1063
1064 if(!can_cast_expr<symbol_exprt>(funcall.function()))
1065 {
1067 "function pointer calls not allowed in frees clauses",
1068 target.source_location());
1069 }
1070
1071 if(type.id() != ID_empty)
1072 {
1074 "expecting void return type for function '" +
1075 id2string(to_symbol_expr(funcall.function()).get_identifier()) +
1076 "' called in frees clause",
1077 target.source_location());
1078 }
1079
1080 for(const auto &argument : funcall.arguments())
1081 throw_on_side_effects(argument);
1082 }
1083 else
1084 {
1085 // anything else is rejected
1087 "frees clause target must be a pointer-typed expression or a call to a "
1088 "function returning void",
1089 target.source_location());
1090 }
1091}
1092
1094{
1095 if(code.find(ID_C_spec_loop_invariant).is_not_nil())
1096 {
1097 for(auto &invariant :
1098 (static_cast<exprt &>(code.add(ID_C_spec_loop_invariant)).operands()))
1099 {
1100 typecheck_expr(invariant);
1101 implicit_typecast_bool(invariant);
1103 invariant,
1104 ID_old,
1105 CPROVER_PREFIX "old is not allowed in loop invariants.");
1106 }
1107 }
1108}
1109
1111{
1112 if(code.find(ID_C_spec_decreases).is_not_nil())
1113 {
1114 for(auto &decreases_clause_component :
1115 (static_cast<exprt &>(code.add(ID_C_spec_decreases)).operands()))
1116 {
1117 typecheck_expr(decreases_clause_component);
1118 implicit_typecast_arithmetic(decreases_clause_component);
1119 }
1120 }
1121}
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: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:250
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
source_locationt end_location() const
Definition std_code.h:187
void add(const codet &code)
Definition std_code.h:168
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
const codet & body() const
Definition std_code.h:565
const exprt & value() const
Definition std_code.h:555
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:134
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
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:39
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
void reserve_operands(operandst::size_type n)
Definition expr.h:150
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:223
source_locationt & add_source_location()
Definition expr.h:228
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:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
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 irep_idt & get_identifier() const
Definition std_expr.h:142
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:3008
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
const exprt & op() const
Definition std_expr.h:326
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1024
#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:47
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
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:361
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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:148
A range is a pair of a begin and an end iterators.
Definition range.h:396
Author: Diffblue Ltd.