cprover
Loading...
Searching...
No Matches
c_typecheck_base.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Conversion / Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "c_typecheck_base.h"
13
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/cprover_prefix.h>
17#include <util/expr_util.h>
19#include <util/std_types.h>
21
23
24#include "ansi_c_declaration.h"
25#include "c_storage_spec.h"
26#include "expr2c.h"
27
28std::string c_typecheck_baset::to_string(const exprt &expr)
29{
30 return expr2c(expr, *this);
31}
32
33std::string c_typecheck_baset::to_string(const typet &type)
34{
35 return type2c(type, *this);
36}
37
39{
40 symbol.mode=mode;
41 symbol.module=module;
42
43 if(symbol_table.move(symbol, new_symbol))
44 {
46 error() << "failed to move symbol '" << symbol.name << "' into symbol table"
47 << eom;
48 throw 0;
49 }
50}
51
53{
54 bool is_function=symbol.type.id()==ID_code;
55
56 const typet &final_type=follow(symbol.type);
57
58 // set a few flags
59 symbol.is_lvalue=!symbol.is_type && !symbol.is_macro;
60
61 irep_idt root_name=symbol.base_name;
62 irep_idt new_name=symbol.name;
63
64 if(symbol.is_file_local)
65 {
66 // file-local stuff -- stays as is
67 // collisions are resolved during linking
68 }
69 else if(symbol.is_extern && !is_function)
70 {
71 // variables marked as "extern" go into the global namespace
72 // and have static lifetime
73 new_name=root_name;
74 symbol.is_static_lifetime=true;
75
76 if(symbol.value.is_not_nil() && !symbol.is_macro)
77 {
78 // According to the C standard this should be an error, but at least some
79 // versions of Visual Studio insist to use this in their C library, and
80 // GCC just warns as well.
82 warning() << "'extern' symbol '" << new_name
83 << "' should not have an initializer" << eom;
84 }
85 }
86 else if(!is_function && symbol.value.id()==ID_code)
87 {
89 error() << "only functions can have a function body" << eom;
90 throw 0;
91 }
92
93 // set the pretty name
94 if(symbol.is_type && final_type.id() == ID_struct)
95 {
96 symbol.pretty_name="struct "+id2string(symbol.base_name);
97 }
98 else if(symbol.is_type && final_type.id() == ID_union)
99 {
100 symbol.pretty_name="union "+id2string(symbol.base_name);
101 }
102 else if(symbol.is_type && final_type.id() == ID_c_enum)
103 {
104 symbol.pretty_name="enum "+id2string(symbol.base_name);
105 }
106 else
107 {
108 symbol.pretty_name=new_name;
109 }
110
111 if(!symbol.is_type && !symbol.is_extern && symbol.type.id() == ID_empty)
112 {
113 error().source_location = symbol.location;
114 error() << "void-typed symbol not permitted" << eom;
115 throw 0;
116 }
117
118 // see if we have it already
119 symbol_table_baset::symbolst::const_iterator old_it =
120 symbol_table.symbols.find(symbol.name);
121
122 if(old_it==symbol_table.symbols.end())
123 {
124 // just put into symbol_table
125 symbolt *new_symbol;
126 move_symbol(symbol, new_symbol);
127
128 typecheck_new_symbol(*new_symbol);
129 }
130 else
131 {
132 if(old_it->second.is_type!=symbol.is_type)
133 {
135 error() << "redeclaration of '" << symbol.display_name()
136 << "' as a different kind of symbol" << eom;
137 throw 0;
138 }
139
140 symbolt &existing_symbol = symbol_table.get_writeable_ref(symbol.name);
141 if(symbol.is_type)
142 typecheck_redefinition_type(existing_symbol, symbol);
143 else
144 typecheck_redefinition_non_type(existing_symbol, symbol);
145 }
146}
147
149{
150 if(symbol.is_parameter)
152
153 // check initializer, if needed
154
155 if(symbol.type.id()==ID_code)
156 {
157 if(symbol.value.is_not_nil() &&
158 !symbol.is_macro)
159 {
161 }
162 else if(
163 symbol.is_macro ||
165 {
166 // we don't need the identifiers
167 for(auto &parameter : to_code_type(symbol.type).parameters())
168 parameter.set_identifier(irep_idt());
169 }
170 }
171 else if(!symbol.is_macro)
172 {
173 // check the initializer
174 do_initializer(symbol);
175 }
176}
177
179 symbolt &old_symbol,
180 symbolt &new_symbol)
181{
182 const typet &final_old=follow(old_symbol.type);
183 const typet &final_new=follow(new_symbol.type);
184
185 // see if we had something incomplete before
186 if(
187 (final_old.id() == ID_struct &&
188 to_struct_type(final_old).is_incomplete()) ||
189 (final_old.id() == ID_union && to_union_type(final_old).is_incomplete()) ||
190 (final_old.id() == ID_c_enum && to_c_enum_type(final_old).is_incomplete()))
191 {
192 // is the new one complete?
193 if(
194 final_new.id() == final_old.id() &&
195 ((final_new.id() == ID_struct &&
196 !to_struct_type(final_new).is_incomplete()) ||
197 (final_new.id() == ID_union &&
198 !to_union_type(final_new).is_incomplete()) ||
199 (final_new.id() == ID_c_enum &&
200 !to_c_enum_type(final_new).is_incomplete())))
201 {
202 // overwrite location
203 old_symbol.location=new_symbol.location;
204
205 // move body
206 old_symbol.type.swap(new_symbol.type);
207 }
208 else if(new_symbol.type.id()==old_symbol.type.id())
209 return; // ignore
210 else
211 {
212 error().source_location=new_symbol.location;
213 error() << "conflicting definition of type symbol '"
214 << new_symbol.display_name() << '\'' << eom;
215 throw 0;
216 }
217 }
218 else
219 {
220 // see if new one is just a tag
221 if(
222 (final_new.id() == ID_struct &&
223 to_struct_type(final_new).is_incomplete()) ||
224 (final_new.id() == ID_union &&
225 to_union_type(final_new).is_incomplete()) ||
226 (final_new.id() == ID_c_enum &&
227 to_c_enum_type(final_new).is_incomplete()))
228 {
229 if(final_old.id() == final_new.id())
230 {
231 // just ignore silently
232 }
233 else
234 {
235 // arg! new tag type
236 error().source_location=new_symbol.location;
237 error() << "conflicting definition of tag symbol '"
238 << new_symbol.display_name() << '\'' << eom;
239 throw 0;
240 }
241 }
243 final_new.id()==ID_c_enum && final_old.id()==ID_c_enum)
244 {
245 // under Windows, ignore this silently;
246 // MSC doesn't think this is a problem, but GCC complains.
247 }
248 else if(
250 final_new.id() == ID_pointer && final_old.id() == ID_pointer &&
251 follow(to_pointer_type(final_new).base_type()).id() == ID_c_enum &&
252 follow(to_pointer_type(final_old).base_type()).id() == ID_c_enum)
253 {
254 // under Windows, ignore this silently;
255 // MSC doesn't think this is a problem, but GCC complains.
256 }
257 else
258 {
259 // see if it changed
260 if(follow(new_symbol.type)!=follow(old_symbol.type))
261 {
262 error().source_location=new_symbol.location;
263 error() << "type symbol '" << new_symbol.display_name()
264 << "' defined twice:\n"
265 << "Original: " << to_string(old_symbol.type) << "\n"
266 << " New: " << to_string(new_symbol.type) << eom;
267 throw 0;
268 }
269 }
270 }
271}
272
274 const struct_typet &old_type,
275 const struct_typet &new_type)
276{
277 const struct_typet::componentst &old_components = old_type.components();
278 const struct_typet::componentst &new_components = new_type.components();
279
280 if(old_components.size() != new_components.size())
281 return false;
282
283 if(old_components.empty())
284 return false;
285
286 for(std::size_t i = 0; i < old_components.size() - 1; ++i)
287 {
288 if(old_components[i].type() != new_components[i].type())
289 return false;
290 }
291
292 if(
293 old_components.back().type().id() != ID_array ||
294 new_components.back().type().id() != ID_array)
295 {
296 return false;
297 }
298
299 const auto &old_array_type = to_array_type(old_components.back().type());
300 const auto &new_array_type = to_array_type(new_components.back().type());
301
302 return old_array_type.element_type() == new_array_type.element_type() &&
303 old_array_type.get_bool(ID_C_flexible_array_member) &&
304 new_array_type.get_bool(ID_C_flexible_array_member) &&
305 (old_array_type.size().is_nil() || old_array_type.size().is_zero());
306}
307
309 symbolt &old_symbol,
310 symbolt &new_symbol)
311{
312 const typet &final_old=follow(old_symbol.type);
313 const typet &initial_new=follow(new_symbol.type);
314
315 if(
316 final_old.id() == ID_array &&
317 to_array_type(final_old).size().is_not_nil() &&
318 initial_new.id() == ID_array &&
319 to_array_type(initial_new).size().is_nil() &&
320 to_array_type(final_old).element_type() ==
321 to_array_type(initial_new).element_type())
322 {
323 // this is ok, just use old type
324 new_symbol.type=old_symbol.type;
325 }
326 else if(
327 final_old.id() == ID_array && to_array_type(final_old).size().is_nil() &&
328 initial_new.id() == ID_array &&
329 to_array_type(initial_new).size().is_not_nil() &&
330 to_array_type(final_old).element_type() ==
331 to_array_type(initial_new).element_type())
332 {
333 // update the type to enable the use of sizeof(x) on the
334 // right-hand side of a definition of x
335 old_symbol.type=new_symbol.type;
336 }
337
338 // do initializer, this may change the type
339 if(new_symbol.type.id() != ID_code && !new_symbol.is_macro)
340 do_initializer(new_symbol);
341
342 const typet &final_new=follow(new_symbol.type);
343
344 // K&R stuff?
345 if(old_symbol.type.id()==ID_KnR)
346 {
347 // check the type
348 if(final_new.id()==ID_code)
349 {
350 error().source_location=new_symbol.location;
351 error() << "function type not allowed for K&R function parameter"
352 << eom;
353 throw 0;
354 }
355
356 // fix up old symbol -- we now got the type
357 old_symbol.type=new_symbol.type;
358 return;
359 }
360
361 if(final_new.id()==ID_code)
362 {
363 if(final_old.id()!=ID_code)
364 {
365 error().source_location=new_symbol.location;
366 error() << "error: function symbol '" << new_symbol.display_name()
367 << "' redefined with a different type:\n"
368 << "Original: " << to_string(old_symbol.type) << "\n"
369 << " New: " << to_string(new_symbol.type) << eom;
370 throw 0;
371 }
372
373 code_typet &old_ct=to_code_type(old_symbol.type);
374 code_typet &new_ct=to_code_type(new_symbol.type);
375
376 if(
377 old_ct.return_type() != new_ct.return_type() &&
378 !old_ct.get_bool(ID_C_incomplete) &&
379 new_ct.return_type().id() != ID_constructor &&
380 new_ct.return_type().id() != ID_destructor)
381 {
382 if(
383 old_ct.return_type().id() == ID_constructor ||
384 old_ct.return_type().id() == ID_destructor)
385 {
386 new_ct = old_ct;
387 }
388 else
389 {
391 "function symbol '" + id2string(new_symbol.display_name()) +
392 "' redefined with a different type:\n" +
393 "Original: " + to_string(old_symbol.type) + "\n" +
394 " New: " + to_string(new_symbol.type),
395 new_symbol.location};
396 }
397 }
398 const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();
399
400 if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
401 old_ct=new_ct;
402 else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis())
403 {
405 {
406 error().source_location = new_symbol.location;
407 error() << "code contract on incomplete function re-declaration" << eom;
408 throw 0;
409 }
410 new_ct=old_ct;
411 }
412
413 if(inlined)
414 {
415 old_ct.set_inlined(true);
416 new_ct.set_inlined(true);
417 }
418
419 // do body
420
421 if(new_symbol.value.is_not_nil())
422 {
423 if(old_symbol.value.is_not_nil())
424 {
425 // gcc allows re-definition if the first
426 // definition is marked as "extern inline"
427
428 if(
429 old_ct.get_inlined() &&
434 {
435 // overwrite "extern inline" properties
436 old_symbol.is_extern=new_symbol.is_extern;
437 old_symbol.is_file_local=new_symbol.is_file_local;
438
439 // remove parameter declarations to avoid conflicts
440 for(const auto &old_parameter : old_ct.parameters())
441 {
442 const irep_idt &identifier = old_parameter.get_identifier();
443
444 symbol_table_baset::symbolst::const_iterator p_s_it =
445 symbol_table.symbols.find(identifier);
446 if(p_s_it!=symbol_table.symbols.end())
447 symbol_table.erase(p_s_it);
448 }
449 }
450 else
451 {
452 error().source_location=new_symbol.location;
453 error() << "function body '" << new_symbol.display_name()
454 << "' defined twice" << eom;
455 throw 0;
456 }
457 }
458 else if(inlined)
459 {
460 // preserve "extern inline" properties
461 old_symbol.is_extern=new_symbol.is_extern;
462 old_symbol.is_file_local=new_symbol.is_file_local;
463 }
464 else if(new_symbol.is_weak)
465 {
466 // weak symbols
467 old_symbol.is_weak=true;
468 }
469
470 if(new_symbol.is_macro)
471 old_symbol.is_macro=true;
472 else
473 typecheck_function_body(new_symbol);
474
475 // overwrite location
476 old_symbol.location=new_symbol.location;
477
478 // move body
479 old_symbol.value.swap(new_symbol.value);
480
481 // overwrite type (because of parameter names)
482 old_symbol.type=new_symbol.type;
483 }
485 {
486 // overwrite type to add contract, but keep the old parameter identifiers
487 // (if any)
488 auto new_parameters_it = new_ct.parameters().begin();
489 for(auto &p : old_ct.parameters())
490 {
491 if(new_parameters_it != new_ct.parameters().end())
492 {
493 new_parameters_it->set_identifier(p.get_identifier());
494 ++new_parameters_it;
495 }
496 }
497
498 old_symbol.type = new_symbol.type;
499 }
500
501 return;
502 }
503
504 if(final_old!=final_new)
505 {
506 if(
507 final_old.id() == ID_array && to_array_type(final_old).size().is_nil() &&
508 final_new.id() == ID_array &&
509 to_array_type(final_new).size().is_not_nil() &&
510 to_array_type(final_old).element_type() ==
511 to_array_type(final_new).element_type())
512 {
513 old_symbol.type=new_symbol.type;
514 }
515 else if(
516 final_old.id() == ID_pointer &&
517 to_pointer_type(final_old).base_type().id() == ID_code &&
518 to_code_type(to_pointer_type(final_old).base_type()).has_ellipsis() &&
519 final_new.id() == ID_pointer &&
520 to_pointer_type(final_new).base_type().id() == ID_code)
521 {
522 // to allow
523 // int (*f) ();
524 // int (*f) (int)=0;
525 old_symbol.type=new_symbol.type;
526 }
527 else if(
528 final_old.id() == ID_pointer &&
529 to_pointer_type(final_old).base_type().id() == ID_code &&
530 final_new.id() == ID_pointer &&
531 to_pointer_type(final_new).base_type().id() == ID_code &&
532 to_code_type(to_pointer_type(final_new).base_type()).has_ellipsis())
533 {
534 // to allow
535 // int (*f) (int)=0;
536 // int (*f) ();
537 }
538 else if(
539 final_old.id() == ID_struct && final_new.id() == ID_struct &&
541 to_struct_type(final_old), to_struct_type(final_new)))
542 {
543 old_symbol.type = new_symbol.type;
544 }
545 else
546 {
547 error().source_location=new_symbol.location;
548 error() << "symbol '" << new_symbol.display_name()
549 << "' redefined with a different type:\n"
550 << "Original: " << to_string(old_symbol.type) << "\n"
551 << " New: " << to_string(new_symbol.type) << eom;
552 throw 0;
553 }
554 }
555 else // finals are equal
556 {
557 }
558
559 // do value
560 if(new_symbol.value.is_not_nil())
561 {
562 // see if we already have one
563 if(old_symbol.value.is_not_nil())
564 {
565 if(
566 new_symbol.is_macro && final_new.id() == ID_c_enum &&
567 old_symbol.value.is_constant() && new_symbol.value.is_constant() &&
568 old_symbol.value.get(ID_value) == new_symbol.value.get(ID_value))
569 {
570 // ignore
571 }
572 else
573 {
575 warning() << "symbol '" << new_symbol.display_name()
576 << "' already has an initial value" << eom;
577 }
578 }
579 else
580 {
581 old_symbol.value=new_symbol.value;
582 old_symbol.type=new_symbol.type;
583 old_symbol.is_macro=new_symbol.is_macro;
584 }
585 }
586
587 // take care of some flags
588 if(old_symbol.is_extern && !new_symbol.is_extern)
589 old_symbol.location=new_symbol.location;
590
591 old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
592
593 // We should likely check is_volatile and
594 // is_thread_local for consistency. GCC complains if these
595 // mismatch.
596}
597
599{
600 if(symbol.value.id() != ID_code)
601 {
602 error().source_location = symbol.location;
603 error() << "function '" << symbol.name << "' is initialized with "
604 << symbol.value.id() << eom;
605 throw 0;
606 }
607
608 code_typet &code_type = to_code_type(symbol.type);
609
610 // reset labels
611 labels_used.clear();
612 labels_defined.clear();
613
614 // A function declaration int foo(); does not specify the parameter list, but
615 // a function definition int foo() { ... } does fix the parameter list to be
616 // empty.
617 if(code_type.parameters().empty() && code_type.has_ellipsis())
618 code_type.remove_ellipsis();
619
620 // fix type
621 symbol.value.type()=code_type;
622
623 // set return type
624 return_type=code_type.return_type();
625
626 // Add the parameter declarations into the symbol table
628
629 // typecheck the body code
631
632 // check the labels
633 for(const auto &label : labels_used)
634 {
635 if(labels_defined.find(label.first) == labels_defined.end())
636 {
637 error().source_location = label.second;
638 error() << "branching label '" << label.first
639 << "' is not defined in function" << eom;
640 throw 0;
641 }
642 }
643}
644
646 const irep_idt &asm_label,
647 symbolt &symbol)
648{
649 const irep_idt orig_name=symbol.name;
650
651 // restrict renaming to functions and global variables;
652 // procedure-local ones would require fixing the scope, as we
653 // do for parameters below
654 if(!asm_label.empty() &&
655 !symbol.is_type &&
656 (symbol.type.id()==ID_code || symbol.is_static_lifetime))
657 {
658 symbol.name=asm_label;
659 symbol.base_name=asm_label;
660 }
661
662 if(symbol.name!=orig_name)
663 {
664 if(!asm_label_map.insert(
665 std::make_pair(orig_name, asm_label)).second)
666 {
667 if(asm_label_map[orig_name]!=asm_label)
668 {
670 error() << "error: replacing asm renaming "
671 << asm_label_map[orig_name] << " by "
672 << asm_label << eom;
673 throw 0;
674 }
675 }
676 }
677 else if(asm_label.empty())
678 {
679 asm_label_mapt::const_iterator entry=
680 asm_label_map.find(symbol.name);
681 if(entry!=asm_label_map.end())
682 {
683 symbol.name=entry->second;
684 symbol.base_name=entry->second;
685 }
686 }
687
688 if(symbol.name!=orig_name &&
689 symbol.type.id()==ID_code &&
690 symbol.value.is_not_nil() && !symbol.is_macro)
691 {
692 const code_typet &code_type=to_code_type(symbol.type);
693
694 for(const auto &p : code_type.parameters())
695 {
696 const irep_idt &p_bn = p.get_base_name();
697 if(p_bn.empty())
698 continue;
699
700 irep_idt p_id=id2string(orig_name)+"::"+id2string(p_bn);
701 irep_idt p_new_id=id2string(symbol.name)+"::"+id2string(p_bn);
702
703 if(!asm_label_map.insert(
704 std::make_pair(p_id, p_new_id)).second)
705 {
706 CHECK_RETURN(asm_label_map[p_id] == p_new_id);
707 }
708 }
709 }
710}
711
713 const exprt &expr,
714 std::string &clause_type)
715{
717 expr, ID_old, CPROVER_PREFIX "old is not allowed in " + clause_type + ".");
719 expr,
720 ID_loop_entry,
721 CPROVER_PREFIX "loop_entry is not allowed in " + clause_type + ".");
722
723 const irep_idt id = CPROVER_PREFIX "return_value";
724 auto pred = [&](const exprt &expr) {
726 return false;
727
728 return to_symbol_expr(expr).get_identifier() == id;
729 };
730
731 if(!has_subexpr(expr, pred))
732 return;
733
735 id2string(id) + " is not allowed in " + id2string(clause_type) + ".",
736 expr.source_location());
737}
738
740 const exprt &expr,
741 std::string &clause_type)
742{
743 const irep_idt id = CPROVER_PREFIX "was_freed";
744
745 auto pred = [&](const exprt &expr) {
747 return false;
748
749 return to_symbol_expr(expr).get_identifier() == id;
750 };
751
752 if(has_subexpr(expr, pred))
753 {
755 id2string(id) + " is not allowed in " + clause_type + ".",
756 expr.source_location());
757 }
758}
759
761 ansi_c_declarationt &declaration)
762{
763 if(declaration.get_is_static_assert())
764 {
765 codet code(ID_static_assert);
766 code.add_source_location() = declaration.source_location();
767 code.operands().swap(declaration.operands());
768 typecheck_code(code);
769 }
770 else
771 {
772 // get storage spec
773 c_storage_spect c_storage_spec(declaration.type());
774
775 // first typecheck the type of the declaration
776 typecheck_type(declaration.type());
777
778 // mark as 'already typechecked'
780
781 // Now do declarators, if any.
782 for(auto &declarator : declaration.declarators())
783 {
784 c_storage_spect full_spec(declaration.full_type(declarator));
785 full_spec|=c_storage_spec;
786
787 declaration.set_is_inline(full_spec.is_inline);
788 declaration.set_is_static(full_spec.is_static);
789 declaration.set_is_extern(full_spec.is_extern);
790 declaration.set_is_thread_local(full_spec.is_thread_local);
791 declaration.set_is_register(full_spec.is_register);
792 declaration.set_is_typedef(full_spec.is_typedef);
793 declaration.set_is_weak(full_spec.is_weak);
794
795 symbolt symbol = declaration.to_symbol(declarator);
796 current_symbol=symbol;
797
798 // now check other half of type
799 typecheck_type(symbol.type);
800
801 if(!full_spec.alias.empty())
802 {
803 if(symbol.value.is_not_nil())
804 {
806 error() << "alias attribute cannot be used with a body"
807 << eom;
808 throw 0;
809 }
810
811 // alias function need not have been declared yet, thus
812 // can't lookup
813 // also cater for renaming/placement in sections
814 const auto &renaming_entry = asm_label_map.find(full_spec.alias);
815 if(renaming_entry == asm_label_map.end())
816 symbol.value = symbol_exprt::typeless(full_spec.alias);
817 else
818 symbol.value = symbol_exprt::typeless(renaming_entry->second);
819 symbol.is_macro=true;
820 }
821
822 if(full_spec.is_used && symbol.is_file_local)
823 {
824 // GCC __attribute__((__used__)) - do not treat those as file-local, but
825 // make sure the name is unique
826 symbol.is_file_local = false;
827
828 symbolt symbol_for_renaming = symbol;
829 if(!full_spec.asm_label.empty())
830 symbol_for_renaming.name = full_spec.asm_label;
831 full_spec.asm_label = djb_manglert{}(
832 symbol_for_renaming,
833 id2string(symbol_for_renaming.location.get_file()));
834 }
835
836 if(full_spec.section.empty())
837 apply_asm_label(full_spec.asm_label, symbol);
838 else
839 {
840 // section name is not empty, do a bit of parsing
841 std::string asm_name = id2string(full_spec.section);
842
843 if(asm_name[0] == '.')
844 {
845 std::string::size_type primary_section = asm_name.find('.', 1);
846
847 if(primary_section != std::string::npos)
848 asm_name.resize(primary_section);
849 }
850
851 asm_name += "$$";
852
853 if(!full_spec.asm_label.empty())
854 asm_name+=id2string(full_spec.asm_label);
855 else
856 asm_name+=id2string(symbol.name);
857
858 apply_asm_label(asm_name, symbol);
859 }
860
861 irep_idt identifier=symbol.name;
862 declarator.set_name(identifier);
863
864 typecheck_symbol(symbol);
865
866 // check the contract, if any
867 symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
868 if(
869 new_symbol.type.id() == ID_code &&
871 {
872 code_with_contract_typet code_type =
874
875 // ensure parameter declarations are available for type checking to
876 // succeed
877 binding_exprt::variablest temporary_parameter_symbols;
878
879 const auto &return_type = code_type.return_type();
880 if(return_type.id() != ID_empty)
881 {
882 parameter_map[CPROVER_PREFIX "return_value"] = return_type;
883 temporary_parameter_symbols.emplace_back(
884 CPROVER_PREFIX "return_value", return_type);
885 }
886
887 std::size_t anon_counter = 0;
888 for(auto &p : code_type.parameters())
889 {
890 // may be anonymous
891 if(p.get_base_name().empty())
892 p.set_base_name("#anon" + std::to_string(anon_counter++));
893
894 // produce identifier
895 const irep_idt &base_name = p.get_base_name();
896 irep_idt parameter_identifier =
897 id2string(identifier) + "::" + id2string(base_name);
898
899 p.set_identifier(parameter_identifier);
900
902 parameter_map.find(parameter_identifier) == parameter_map.end());
903 parameter_map[parameter_identifier] = p.type();
904 temporary_parameter_symbols.emplace_back(
905 parameter_identifier, p.type());
906 }
907
908 for(auto &c_requires : code_type.c_requires())
909 {
910 typecheck_expr(c_requires);
911 implicit_typecast_bool(c_requires);
912 std::string clause_type = "preconditions";
913 check_history_expr_return_value(c_requires, clause_type);
914 check_was_freed(c_requires, clause_type);
915 lambda_exprt lambda{temporary_parameter_symbols, c_requires};
916 lambda.add_source_location() = c_requires.source_location();
917 c_requires.swap(lambda);
918 }
919
921 for(auto &assigns : code_type.c_assigns())
922 {
923 std::string clause_type = "assigns clauses";
924 check_history_expr_return_value(assigns, clause_type);
925 lambda_exprt lambda{temporary_parameter_symbols, assigns};
926 lambda.add_source_location() = assigns.source_location();
927 assigns.swap(lambda);
928 }
929
930 typecheck_spec_frees(code_type.c_frees());
931 for(auto &frees : code_type.c_frees())
932 {
933 lambda_exprt lambda{temporary_parameter_symbols, frees};
934 lambda.add_source_location() = frees.source_location();
935 frees.swap(lambda);
936 }
937
938 for(auto &ensures : code_type.c_ensures())
939 {
940 typecheck_expr(ensures);
941 implicit_typecast_bool(ensures);
943 ensures,
944 ID_loop_entry,
945 CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
946 lambda_exprt lambda{temporary_parameter_symbols, ensures};
947 lambda.add_source_location() = ensures.source_location();
948 ensures.swap(lambda);
949 }
950
951 for(const auto &parameter_sym : temporary_parameter_symbols)
952 parameter_map.erase(parameter_sym.get_identifier());
953
954 // create a contract symbol
955 symbolt contract;
956 contract.name = "contract::" + id2string(new_symbol.name);
957 contract.base_name = new_symbol.base_name;
958 contract.pretty_name = new_symbol.pretty_name;
959 contract.is_property = true;
960 contract.type = code_type;
961 contract.mode = new_symbol.mode;
962 contract.module = module;
963 contract.location = new_symbol.location;
964
965 auto entry = symbol_table.insert(std::move(contract));
966 if(!entry.second)
967 {
968 error().source_location = new_symbol.location;
969 error() << "contract '" << new_symbol.display_name()
970 << "' already set at " << entry.first.location.as_string()
971 << eom;
972 throw 0;
973 }
974
975 // Remove the contract from the original symbol as we have created a
976 // dedicated contract symbol.
977 new_symbol.type.remove(ID_C_spec_assigns);
978 new_symbol.type.remove(ID_C_spec_frees);
979 new_symbol.type.remove(ID_C_spec_ensures);
980 new_symbol.type.remove(ID_C_spec_requires);
981 }
982 }
983 }
984}
985
987{
989
990 code_typet &code_type = to_code_type(symbol.type);
991
992 unsigned anon_counter = 0;
993
994 // Add the parameter declarations into the symbol table.
995 for(auto &p : code_type.parameters())
996 {
997 // may be anonymous
998 if(p.get_base_name().empty())
999 {
1000 irep_idt base_name = "#anon" + std::to_string(anon_counter++);
1001 p.set_base_name(base_name);
1002 }
1003
1004 // produce identifier
1005 irep_idt base_name = p.get_base_name();
1006 irep_idt identifier = id2string(symbol.name) + "::" + id2string(base_name);
1007
1008 p.set_identifier(identifier);
1009
1010 parameter_symbolt p_symbol;
1011
1012 p_symbol.type = p.type();
1013 p_symbol.name = identifier;
1014 p_symbol.base_name = base_name;
1015 p_symbol.location = p.source_location();
1016
1017 symbolt *new_p_symbol;
1018 move_symbol(p_symbol, new_p_symbol);
1019 }
1020}
ANSI-CC Language Type Checking.
configt config
Definition config.cpp:25
static bool is_instantiation_of_flexible_array(const struct_typet &old_type, const struct_typet &new_type)
ANSI-C Language Type Checking.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition c_types.h:467
static void make_already_typechecked(typet &type)
void set_is_thread_local(bool is_thread_local)
void set_is_weak(bool is_weak)
symbolt to_symbol(const ansi_c_declaratort &) const
const declaratorst & declarators() const
void set_is_register(bool is_register)
void set_is_inline(bool is_inline)
typet full_type(const ansi_c_declaratort &) const
void set_is_extern(bool is_extern)
void set_is_typedef(bool is_typedef)
bool get_is_static_assert() const
void set_is_static(bool is_static)
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
std::vector< symbol_exprt > variablest
Definition std_expr.h:3054
symbol_table_baset & symbol_table
virtual void check_history_expr_return_value(const exprt &expr, std::string &clause_type)
Checks that no history expr or return_value exists in expr.
void typecheck_function_body(symbolt &symbol)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void check_was_freed(const exprt &expr, std::string &clause_type)
Checks that no occurence of the CPROVER_PREFIX was_freed predicate is found in expr.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
const irep_idt mode
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
void typecheck_new_symbol(symbolt &symbol)
asm_label_mapt asm_label_map
virtual void adjust_function_parameter(typet &type) const
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
void add_parameters_to_symbol_table(symbolt &symbol)
Create symbols for parameter of the code-typed symbol symbol.
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void typecheck_spec_frees(exprt::operandst &targets)
virtual void typecheck_spec_assigns(exprt::operandst &targets)
id_type_mapt parameter_map
virtual void implicit_typecast_bool(exprt &expr)
virtual void typecheck_type(typet &type)
void typecheck_symbol(symbolt &symbol)
std::map< irep_idt, source_locationt > labels_defined
Base type of functions.
Definition std_types.h:539
void set_inlined(bool value)
Definition std_types.h:670
bool get_inlined() const
Definition std_types.h:665
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
void remove_ellipsis()
Definition std_types.h:640
bool has_ellipsis() const
Definition std_types.h:611
const exprt::operandst & c_frees() const
Definition c_types.h:418
const exprt::operandst & c_assigns() const
Definition c_types.h:408
const exprt::operandst & c_requires() const
Definition c_types.h:428
const exprt::operandst & c_ensures() const
Definition c_types.h:438
bool has_contract() const
Definition c_types.h:402
Data structure for representing an arbitrary statement in a program.
struct configt::ansi_ct ansi_c
Mangle identifiers by hashing their working directory with djb2 hash.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
const std::string & as_string() const
Definition dstring.h:215
bool empty() const
Definition dstring.h:90
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
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
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
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:95
bool is_not_nil() const
Definition irep.h:380
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
A (mathematical) lambda expression.
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
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition symbol.h:179
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_file() const
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:132
const irep_idt & get_identifier() const
Definition std_expr.h:142
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
bool is_file_local
Definition symbol.h:73
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
bool is_static_lifetime
Definition symbol.h:70
bool is_property
Definition symbol.h:67
bool is_parameter
Definition symbol.h:76
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
bool is_weak
Definition symbol.h:78
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
bool is_lvalue
Definition symbol.h:72
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4144
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4160
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.
bool has_contract(const irep_idt &function_identifier, const namespacet &ns)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for 'mathematical' expressions.
Mangle names of file-local functions to make them unique.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const codet & to_code(const exprt &expr)
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
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition std_types.h:731
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
flavourt mode
Definition config.h:249
Author: Diffblue Ltd.