cprover
Loading...
Searching...
No Matches
linking.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Linking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "linking.h"
13
14#include <deque>
15#include <unordered_set>
16
17#include <util/base_type.h>
18#include <util/c_types.h>
19#include <util/find_symbols.h>
21#include <util/pointer_expr.h>
23#include <util/simplify_expr.h>
24#include <util/symbol_table.h>
25
27
28#include "linking_class.h"
29
31{
32 expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
33
34 if(it == expr_map.end())
35 return true;
36
37 const exprt &e = it->second;
38
39 if(e.type().id() != ID_array)
40 {
41 typet type = s.type();
42 static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
43 }
44 else
45 static_cast<exprt &>(s) = e;
46
47 return false;
48}
49
51 const irep_idt &identifier,
52 const exprt &expr) const
53{
54 return from_expr(ns, identifier, expr);
55}
56
58 const irep_idt &identifier,
59 const typet &type) const
60{
61 return from_type(ns, identifier, type);
62}
63
65 const namespacet &ns,
66 const typet &type)
67{
68 if(type.id() == ID_c_enum_tag)
69 return ns.follow_tag(to_c_enum_tag_type(type));
70 else if(type.id()==ID_struct_tag)
71 return ns.follow_tag(to_struct_tag_type(type));
72 else if(type.id()==ID_union_tag)
73 return ns.follow_tag(to_union_tag_type(type));
74 else
75 return type;
76}
77
79 const symbolt &symbol,
80 const typet &type) const
81{
82 const typet &followed=follow_tags_symbols(ns, type);
83
84 if(followed.id()==ID_struct || followed.id()==ID_union)
85 {
86 std::string result=followed.id_string();
87
88 const std::string &tag=followed.get_string(ID_tag);
89 if(!tag.empty())
90 result+=" "+tag;
91
92 if(to_struct_union_type(followed).is_incomplete())
93 {
94 result += " (incomplete)";
95 }
96 else
97 {
98 result += " {\n";
99
100 for(const auto &c : to_struct_union_type(followed).components())
101 {
102 const typet &subtype = c.type();
103 result += " ";
104 result += type_to_string(symbol.name, subtype);
105 result += ' ';
106
107 if(!c.get_base_name().empty())
108 result += id2string(c.get_base_name());
109 else
110 result += id2string(c.get_name());
111
112 result += ";\n";
113 }
114
115 result += '}';
116 }
117
118 return result;
119 }
120 else if(followed.id()==ID_pointer)
121 {
123 symbol, to_pointer_type(followed).base_type()) +
124 " *";
125 }
126
127 return type_to_string(symbol.name, type);
128}
129
131 const symbolt &old_symbol,
132 const symbolt &new_symbol,
133 const typet &type1,
134 const typet &type2,
135 unsigned depth,
136 exprt &conflict_path)
137{
138 #ifdef DEBUG
139 debug() << "<BEGIN DEPTH " << depth << ">" << eom;
140 #endif
141
142 std::string msg;
143
144 const typet &t1=follow_tags_symbols(ns, type1);
145 const typet &t2=follow_tags_symbols(ns, type2);
146
147 if(t1.id()!=t2.id())
148 msg="type classes differ";
149 else if(t1.id()==ID_pointer ||
150 t1.id()==ID_array)
151 {
152 if(
153 depth > 0 && !base_type_eq(
154 to_type_with_subtype(t1).subtype(),
155 to_type_with_subtype(t2).subtype(),
156 ns))
157 {
158 if(conflict_path.type().id() == ID_pointer)
159 conflict_path = dereference_exprt(conflict_path);
160
162 old_symbol,
163 new_symbol,
164 to_type_with_subtype(t1).subtype(),
165 to_type_with_subtype(t2).subtype(),
166 depth - 1,
167 conflict_path);
168 }
169 else if(t1.id()==ID_pointer)
170 msg="pointer types differ";
171 else
172 msg="array types differ";
173 }
174 else if(t1.id()==ID_struct ||
175 t1.id()==ID_union)
176 {
177 const struct_union_typet::componentst &components1=
179
180 const struct_union_typet::componentst &components2=
182
183 exprt conflict_path_before=conflict_path;
184
185 if(components1.size()!=components2.size())
186 {
187 msg="number of members is different (";
188 msg+=std::to_string(components1.size())+'/';
189 msg+=std::to_string(components2.size())+')';
190 }
191 else
192 {
193 for(std::size_t i=0; i<components1.size(); ++i)
194 {
195 const typet &subtype1=components1[i].type();
196 const typet &subtype2=components2[i].type();
197
198 if(components1[i].get_name()!=components2[i].get_name())
199 {
200 msg="names of member "+std::to_string(i)+" differ (";
201 msg+=id2string(components1[i].get_name())+'/';
202 msg+=id2string(components2[i].get_name())+')';
203 break;
204 }
205 else if(!base_type_eq(subtype1, subtype2, ns))
206 {
207 typedef std::unordered_set<typet, irep_hash> type_sett;
208 type_sett parent_types;
209
210 exprt e=conflict_path_before;
211 while(e.id()==ID_dereference ||
212 e.id()==ID_member ||
213 e.id()==ID_index)
214 {
215 parent_types.insert(e.type());
216 if(e.id() == ID_dereference)
218 else if(e.id() == ID_member)
219 e = to_member_expr(e).compound();
220 else if(e.id() == ID_index)
221 e = to_index_expr(e).array();
222 else
224 }
225
226 conflict_path=conflict_path_before;
227 conflict_path.type()=t1;
228 conflict_path=
229 member_exprt(conflict_path, components1[i]);
230
231 if(depth>0 &&
232 parent_types.find(t1)==parent_types.end())
234 old_symbol,
235 new_symbol,
236 subtype1,
237 subtype2,
238 depth-1,
239 conflict_path);
240 else
241 {
242 msg="type of member "+
243 id2string(components1[i].get_name())+
244 " differs";
245 if(depth>0)
246 {
247 std::string msg_bak;
248 msg_bak.swap(msg);
251 old_symbol,
252 new_symbol,
253 subtype1,
254 subtype2,
255 depth-1,
256 c);
257 msg.swap(msg_bak);
258 }
259 }
260
261 if(parent_types.find(t1)==parent_types.end())
262 break;
263 }
264 }
265 }
266 }
267 else if(t1.id()==ID_c_enum)
268 {
269 const c_enum_typet::memberst &members1=
271
272 const c_enum_typet::memberst &members2=
274
275 if(
276 to_c_enum_type(t1).underlying_type() !=
277 to_c_enum_type(t2).underlying_type())
278 {
279 msg="enum value types are different (";
280 msg +=
281 type_to_string(old_symbol.name, to_c_enum_type(t1).underlying_type()) +
282 '/';
283 msg +=
284 type_to_string(new_symbol.name, to_c_enum_type(t2).underlying_type()) +
285 ')';
286 }
287 else if(members1.size()!=members2.size())
288 {
289 msg="number of enum members is different (";
290 msg+=std::to_string(members1.size())+'/';
291 msg+=std::to_string(members2.size())+')';
292 }
293 else
294 {
295 for(std::size_t i=0; i<members1.size(); ++i)
296 {
297 if(members1[i].get_base_name()!=members2[i].get_base_name())
298 {
299 msg="names of member "+std::to_string(i)+" differ (";
300 msg+=id2string(members1[i].get_base_name())+'/';
301 msg+=id2string(members2[i].get_base_name())+')';
302 break;
303 }
304 else if(members1[i].get_value()!=members2[i].get_value())
305 {
306 msg="values of member "+std::to_string(i)+" differ (";
307 msg+=id2string(members1[i].get_value())+'/';
308 msg+=id2string(members2[i].get_value())+')';
309 break;
310 }
311 }
312 }
313
314 msg+="\nenum declarations at\n";
315 msg+=t1.source_location().as_string()+" and\n";
316 msg+=t1.source_location().as_string();
317 }
318 else if(t1.id()==ID_code)
319 {
320 const code_typet::parameterst &parameters1=
322
323 const code_typet::parameterst &parameters2=
325
326 const typet &return_type1=to_code_type(t1).return_type();
327 const typet &return_type2=to_code_type(t2).return_type();
328
329 if(parameters1.size()!=parameters2.size())
330 {
331 msg="parameter counts differ (";
332 msg+=std::to_string(parameters1.size())+'/';
333 msg+=std::to_string(parameters2.size())+')';
334 }
335 else if(!base_type_eq(return_type1, return_type2, ns))
336 {
337 conflict_path=
338 index_exprt(conflict_path,
339 constant_exprt(std::to_string(-1), integer_typet()));
340
341 if(depth>0)
343 old_symbol,
344 new_symbol,
345 return_type1,
346 return_type2,
347 depth-1,
348 conflict_path);
349 else
350 msg="return types differ";
351 }
352 else
353 {
354 for(std::size_t i=0; i<parameters1.size(); i++)
355 {
356 const typet &subtype1=parameters1[i].type();
357 const typet &subtype2=parameters2[i].type();
358
359 if(!base_type_eq(subtype1, subtype2, ns))
360 {
361 conflict_path=
362 index_exprt(conflict_path,
363 constant_exprt(std::to_string(i), integer_typet()));
364
365 if(depth>0)
367 old_symbol,
368 new_symbol,
369 subtype1,
370 subtype2,
371 depth-1,
372 conflict_path);
373 else
374 msg="parameter types differ";
375
376 break;
377 }
378 }
379 }
380 }
381 else
382 msg="conflict on POD";
383
384 if(!msg.empty())
385 {
386 error() << '\n';
387 error() << "reason for conflict at "
388 << expr_to_string(irep_idt(), conflict_path) << ": " << msg << '\n';
389
390 error() << '\n';
391 error() << type_to_string_verbose(old_symbol, t1) << '\n';
392 error() << type_to_string_verbose(new_symbol, t2) << '\n';
393 }
394
395 #ifdef DEBUG
396 debug() << "<END DEPTH " << depth << ">" << eom;
397 #endif
398}
399
401 const symbolt &old_symbol,
402 const symbolt &new_symbol,
403 const std::string &msg)
404{
405 error().source_location=new_symbol.location;
406
407 error() << "error: " << msg << " '" << old_symbol.display_name() << "'"
408 << '\n';
409 error() << "old definition in module '" << old_symbol.module << "' "
410 << old_symbol.location << '\n'
411 << type_to_string_verbose(old_symbol) << '\n';
412 error() << "new definition in module '" << new_symbol.module << "' "
413 << new_symbol.location << '\n'
414 << type_to_string_verbose(new_symbol) << eom;
415}
416
418 const symbolt &old_symbol,
419 const symbolt &new_symbol,
420 const std::string &msg)
421{
422 warning().source_location=new_symbol.location;
423
424 warning() << "warning: " << msg << " \""
425 << old_symbol.display_name()
426 << "\"" << '\n';
427 warning() << "old definition in module " << old_symbol.module << " "
428 << old_symbol.location << '\n'
429 << type_to_string_verbose(old_symbol) << '\n';
430 warning() << "new definition in module " << new_symbol.module << " "
431 << new_symbol.location << '\n'
432 << type_to_string_verbose(new_symbol) << eom;
433}
434
436{
437 unsigned cnt=0;
438
439 while(true)
440 {
441 irep_idt new_identifier=
442 id2string(id)+"$link"+std::to_string(++cnt);
443
444 if(main_symbol_table.symbols.find(new_identifier)!=
446 continue; // already in main symbol table
447
448 if(!renamed_ids.insert(new_identifier).second)
449 continue; // used this for renaming already
450
451 if(src_symbol_table.symbols.find(new_identifier)!=
453 continue; // used by some earlier linking call already
454
455 return new_identifier;
456 }
457}
458
460 const symbolt &old_symbol,
461 const symbolt &new_symbol)
462{
463 // We first take care of file-local non-type symbols.
464 // These are static functions, or static variables
465 // inside static function bodies.
466 if(new_symbol.is_file_local ||
467 old_symbol.is_file_local)
468 return true;
469
470 return false;
471}
472
474 symbolt &old_symbol,
475 symbolt &new_symbol)
476{
477 // Both are functions.
478 if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
479 {
480 const code_typet &old_t=to_code_type(old_symbol.type);
481 const code_typet &new_t=to_code_type(new_symbol.type);
482
483 // if one of them was an implicit declaration then only conflicts on the
484 // return type are an error as we would end up with assignments with
485 // mismatching types; as we currently do not patch these by inserting type
486 // casts we need to fail hard
487 if(old_symbol.type.get_bool(ID_C_incomplete) && old_symbol.value.is_nil())
488 {
489 if(base_type_eq(old_t.return_type(), new_t.return_type(), ns))
491 old_symbol,
492 new_symbol,
493 "implicit function declaration");
494 else
496 old_symbol,
497 new_symbol,
498 "implicit function declaration");
499
500 old_symbol.type=new_symbol.type;
501 old_symbol.location=new_symbol.location;
502 old_symbol.is_weak=new_symbol.is_weak;
503 }
504 else if(
505 new_symbol.type.get_bool(ID_C_incomplete) && new_symbol.value.is_nil())
506 {
507 if(base_type_eq(old_t.return_type(), new_t.return_type(), ns))
509 old_symbol,
510 new_symbol,
511 "ignoring conflicting implicit function declaration");
512 else
514 old_symbol,
515 new_symbol,
516 "implicit function declaration");
517 }
518 // handle (incomplete) function prototypes
519 else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
520 ((old_t.parameters().empty() &&
521 old_t.has_ellipsis() &&
522 old_symbol.value.is_nil()) ||
523 (new_t.parameters().empty() &&
524 new_t.has_ellipsis() &&
525 new_symbol.value.is_nil())))
526 {
527 if(old_t.parameters().empty() &&
528 old_t.has_ellipsis() &&
529 old_symbol.value.is_nil())
530 {
531 old_symbol.type=new_symbol.type;
532 old_symbol.location=new_symbol.location;
533 old_symbol.is_weak=new_symbol.is_weak;
534 }
535 }
536 // replace weak symbols
537 else if(old_symbol.is_weak)
538 {
539 if(new_symbol.value.is_nil())
541 old_symbol,
542 new_symbol,
543 "function declaration conflicts with with weak definition");
544 else
545 old_symbol.value.make_nil();
546 }
547 else if(new_symbol.is_weak)
548 {
549 if(new_symbol.value.is_nil() ||
550 old_symbol.value.is_not_nil())
551 {
552 new_symbol.value.make_nil();
553
555 old_symbol,
556 new_symbol,
557 "ignoring conflicting weak function declaration");
558 }
559 }
560 // aliasing may alter the type
561 else if((new_symbol.is_macro &&
562 new_symbol.value.is_not_nil() &&
563 old_symbol.value.is_nil()) ||
564 (old_symbol.is_macro &&
565 old_symbol.value.is_not_nil() &&
566 new_symbol.value.is_nil()))
567 {
569 old_symbol,
570 new_symbol,
571 "ignoring conflicting function alias declaration");
572 }
573 // conflicting declarations without a definition, matching return
574 // types
575 else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
576 old_symbol.value.is_nil() &&
577 new_symbol.value.is_nil())
578 {
580 old_symbol,
581 new_symbol,
582 "ignoring conflicting function declarations");
583
584 if(old_t.parameters().size()<new_t.parameters().size())
585 {
586 old_symbol.type=new_symbol.type;
587 old_symbol.location=new_symbol.location;
588 old_symbol.is_weak=new_symbol.is_weak;
589 }
590 }
591 // mismatch on number of parameters is definitively an error
592 else if((old_t.parameters().size()<new_t.parameters().size() &&
593 new_symbol.value.is_not_nil() &&
594 !old_t.has_ellipsis()) ||
595 (old_t.parameters().size()>new_t.parameters().size() &&
596 old_symbol.value.is_not_nil() &&
597 !new_t.has_ellipsis()))
598 {
600 old_symbol,
601 new_symbol,
602 "conflicting parameter counts of function declarations");
603
604 // error logged, continue typechecking other symbols
605 return;
606 }
607 else
608 {
609 // the number of parameters matches, collect all the conflicts
610 // and see whether they can be cured
611 std::string warn_msg;
612 bool replace=false;
613 typedef std::deque<std::pair<typet, typet> > conflictst;
614 conflictst conflicts;
615
616 if(!base_type_eq(old_t.return_type(), new_t.return_type(), ns))
617 conflicts.push_back(
618 std::make_pair(old_t.return_type(), new_t.return_type()));
619
620 code_typet::parameterst::const_iterator
621 n_it=new_t.parameters().begin(),
622 o_it=old_t.parameters().begin();
623 for( ;
624 o_it!=old_t.parameters().end() &&
625 n_it!=new_t.parameters().end();
626 ++o_it, ++n_it)
627 {
628 if(!base_type_eq(o_it->type(), n_it->type(), ns))
629 conflicts.push_back(
630 std::make_pair(o_it->type(), n_it->type()));
631 }
632 if(o_it!=old_t.parameters().end())
633 {
634 if(!new_t.has_ellipsis() && old_symbol.value.is_not_nil())
635 {
637 old_symbol,
638 new_symbol,
639 "conflicting parameter counts of function declarations");
640
641 // error logged, continue typechecking other symbols
642 return;
643 }
644
645 replace=new_symbol.value.is_not_nil();
646 }
647 else if(n_it!=new_t.parameters().end())
648 {
649 if(!old_t.has_ellipsis() && new_symbol.value.is_not_nil())
650 {
652 old_symbol,
653 new_symbol,
654 "conflicting parameter counts of function declarations");
655
656 // error logged, continue typechecking other symbols
657 return;
658 }
659
660 replace=new_symbol.value.is_not_nil();
661 }
662
663 while(!conflicts.empty())
664 {
665 const typet &t1=follow_tags_symbols(ns, conflicts.front().first);
666 const typet &t2=follow_tags_symbols(ns, conflicts.front().second);
667
668 // void vs. non-void return type may be acceptable if the
669 // return value is never used
670 if((t1.id()==ID_empty || t2.id()==ID_empty) &&
671 (old_symbol.value.is_nil() || new_symbol.value.is_nil()))
672 {
673 if(warn_msg.empty())
674 warn_msg="void/non-void return type conflict on function";
675 replace=
676 new_symbol.value.is_not_nil() ||
677 (old_symbol.value.is_nil() && t2.id()==ID_empty);
678 }
679 // different pointer arguments without implementation may work
680 else if((t1.id()==ID_pointer || t2.id()==ID_pointer) &&
682 old_symbol.value.is_nil() && new_symbol.value.is_nil())
683 {
684 if(warn_msg.empty())
685 warn_msg="different pointer types in extern function";
686 }
687 // different pointer arguments with implementation - the
688 // implementation is always right, even though such code may
689 // be severely broken
690 else if((t1.id()==ID_pointer || t2.id()==ID_pointer) &&
692 old_symbol.value.is_nil()!=new_symbol.value.is_nil())
693 {
694 if(warn_msg.empty())
695 warn_msg="pointer parameter types differ between "
696 "declaration and definition";
697 replace=new_symbol.value.is_not_nil();
698 }
699 // transparent union with (or entirely without) implementation is
700 // ok -- this primarily helps all those people that don't get
701 // _GNU_SOURCE consistent
702 else if((t1.id()==ID_union &&
703 (t1.get_bool(ID_C_transparent_union) ||
704 conflicts.front().first.get_bool(ID_C_transparent_union))) ||
705 (t2.id()==ID_union &&
706 (t2.get_bool(ID_C_transparent_union) ||
707 conflicts.front().second.get_bool(ID_C_transparent_union))))
708 {
709 const bool use_old=
710 t1.id()==ID_union &&
711 (t1.get_bool(ID_C_transparent_union) ||
712 conflicts.front().first.get_bool(ID_C_transparent_union)) &&
713 new_symbol.value.is_nil();
714
715 const union_typet &union_type=
716 to_union_type(t1.id()==ID_union?t1:t2);
717 const typet &src_type=t1.id()==ID_union?t2:t1;
718
719 bool found=false;
720 for(const auto &c : union_type.components())
721 if(base_type_eq(c.type(), src_type, ns))
722 {
723 found=true;
724 if(warn_msg.empty())
725 warn_msg="conflict on transparent union parameter in function";
726 replace=!use_old;
727 }
728
729 if(!found)
730 break;
731 }
732 // different non-pointer arguments with implementation - the
733 // implementation is always right, even though such code may
734 // be severely broken
735 else if(pointer_offset_bits(t1, ns)==pointer_offset_bits(t2, ns) &&
736 old_symbol.value.is_nil()!=new_symbol.value.is_nil())
737 {
738 if(warn_msg.empty())
739 warn_msg="non-pointer parameter types differ between "
740 "declaration and definition";
741 replace=new_symbol.value.is_not_nil();
742 }
743 else
744 break;
745
746 conflicts.pop_front();
747 }
748
749 if(!conflicts.empty())
750 {
752 old_symbol,
753 new_symbol,
754 conflicts.front().first,
755 conflicts.front().second);
756
758 old_symbol,
759 new_symbol,
760 "conflicting function declarations");
761
762 // error logged, continue typechecking other symbols
763 return;
764 }
765 else
766 {
767 // warns about the first inconsistency
768 link_warning(old_symbol, new_symbol, warn_msg);
769
770 if(replace)
771 {
772 old_symbol.type=new_symbol.type;
773 old_symbol.location=new_symbol.location;
774 }
775 }
776 }
777 }
778
779 if(!new_symbol.value.is_nil())
780 {
781 if(old_symbol.value.is_nil())
782 {
783 // the one with body wins!
784 rename_symbol(new_symbol.value);
785 rename_symbol(new_symbol.type);
786 old_symbol.value=new_symbol.value;
787 old_symbol.type=new_symbol.type; // for parameter identifiers
788 old_symbol.is_weak=new_symbol.is_weak;
789 old_symbol.location=new_symbol.location;
790 old_symbol.is_macro=new_symbol.is_macro;
791 }
792 else if(to_code_type(old_symbol.type).get_inlined())
793 {
794 // ok, silently ignore
795 }
796 else if(base_type_eq(old_symbol.type, new_symbol.type, ns))
797 {
798 // keep the one in old_symbol -- libraries come last!
799 warning().source_location=new_symbol.location;
800
801 warning() << "function '" << old_symbol.name << "' in module '"
802 << new_symbol.module
803 << "' is shadowed by a definition in module '"
804 << old_symbol.module << "'" << eom;
805 }
806 else
808 old_symbol,
809 new_symbol,
810 "duplicate definition of function");
811 }
812}
813
815 const typet &t1,
816 const typet &t2,
817 adjust_type_infot &info)
818{
819 if(base_type_eq(t1, t2, ns))
820 return false;
821
822 if(
823 t1.id() == ID_struct_tag || t1.id() == ID_union_tag ||
824 t1.id() == ID_c_enum_tag)
825 {
826 const irep_idt &identifier = to_tag_type(t1).get_identifier();
827
828 if(info.o_symbols.insert(identifier).second)
829 {
830 bool result=
832 info.o_symbols.erase(identifier);
833
834 return result;
835 }
836
837 return false;
838 }
839 else if(
840 t2.id() == ID_struct_tag || t2.id() == ID_union_tag ||
841 t2.id() == ID_c_enum_tag)
842 {
843 const irep_idt &identifier = to_tag_type(t2).get_identifier();
844
845 if(info.n_symbols.insert(identifier).second)
846 {
847 bool result=
849 info.n_symbols.erase(identifier);
850
851 return result;
852 }
853
854 return false;
855 }
856 else if(t1.id()==ID_pointer && t2.id()==ID_array)
857 {
858 info.set_to_new=true; // store new type
859
860 return false;
861 }
862 else if(t1.id()==ID_array && t2.id()==ID_pointer)
863 {
864 // ignore
865 return false;
866 }
867 else if(
868 t1.id() == ID_struct && to_struct_type(t1).is_incomplete() &&
869 t2.id() == ID_struct && !to_struct_type(t2).is_incomplete())
870 {
871 info.set_to_new=true; // store new type
872
873 return false;
874 }
875 else if(
876 t1.id() == ID_union && to_union_type(t1).is_incomplete() &&
877 t2.id() == ID_union && !to_union_type(t2).is_incomplete())
878 {
879 info.set_to_new = true; // store new type
880
881 return false;
882 }
883 else if(
884 t1.id() == ID_struct && !to_struct_type(t1).is_incomplete() &&
885 t2.id() == ID_struct && to_struct_type(t2).is_incomplete())
886 {
887 // ignore
888 return false;
889 }
890 else if(
891 t1.id() == ID_union && !to_union_type(t1).is_incomplete() &&
892 t2.id() == ID_union && to_union_type(t2).is_incomplete())
893 {
894 // ignore
895 return false;
896 }
897 else if(t1.id()!=t2.id())
898 {
899 // type classes do not match and can't be fixed
900 return true;
901 }
902
903 if(t1.id()==ID_pointer)
904 {
905 #if 0
906 bool s=info.set_to_new;
907 if(adjust_object_type_rec(t1.subtype(), t2.subtype(), info))
908 {
910 info.old_symbol,
911 info.new_symbol,
912 "conflicting pointer types for variable");
913 info.set_to_new=s;
914 }
915 #else
917 info.old_symbol,
918 info.new_symbol,
919 "conflicting pointer types for variable");
920 #endif
921
922 if(info.old_symbol.is_extern && !info.new_symbol.is_extern)
923 {
924 info.set_to_new = true; // store new type
925 }
926
927 return false;
928 }
929 else if(
930 t1.id() == ID_array &&
932 to_array_type(t1).element_type(), to_array_type(t2).element_type(), info))
933 {
934 // still need to compare size
935 const exprt &old_size=to_array_type(t1).size();
936 const exprt &new_size=to_array_type(t2).size();
937
938 if((old_size.is_nil() && new_size.is_not_nil()) ||
939 (old_size.is_zero() && new_size.is_not_nil()) ||
940 info.old_symbol.is_weak)
941 {
942 info.set_to_new=true; // store new type
943 }
944 else if(new_size.is_nil() ||
945 new_size.is_zero() ||
946 info.new_symbol.is_weak)
947 {
948 // ok, we will use the old type
949 }
950 else
951 {
952 equal_exprt eq(old_size, new_size);
953
954 if(!simplify_expr(eq, ns).is_true())
955 {
957 info.old_symbol,
958 info.new_symbol,
959 "conflicting array sizes for variable");
960
961 // error logged, continue typechecking other symbols
962 return true;
963 }
964 }
965
966 return false;
967 }
968 else if(t1.id()==ID_struct || t1.id()==ID_union)
969 {
970 const struct_union_typet::componentst &components1=
972
973 const struct_union_typet::componentst &components2=
975
976 struct_union_typet::componentst::const_iterator
977 it1=components1.begin(), it2=components2.begin();
978 for( ;
979 it1!=components1.end() && it2!=components2.end();
980 ++it1, ++it2)
981 {
982 if(it1->get_name()!=it2->get_name() ||
983 adjust_object_type_rec(it1->type(), it2->type(), info))
984 return true;
985 }
986 if(it1!=components1.end() || it2!=components2.end())
987 return true;
988
989 return false;
990 }
991
992 return true;
993}
994
996 const symbolt &old_symbol,
997 const symbolt &new_symbol,
998 bool &set_to_new)
999{
1000 const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
1001 const typet &new_type=follow_tags_symbols(ns, new_symbol.type);
1002
1003 adjust_type_infot info(old_symbol, new_symbol);
1004 bool result=adjust_object_type_rec(old_type, new_type, info);
1005 set_to_new=info.set_to_new;
1006
1007 return result;
1008}
1009
1011 symbolt &old_symbol,
1012 symbolt &new_symbol)
1013{
1014 // both are variables
1015 bool set_to_new = false;
1016
1017 if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
1018 {
1019 bool failed=
1020 adjust_object_type(old_symbol, new_symbol, set_to_new);
1021
1022 if(failed)
1023 {
1024 const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
1025
1026 // provide additional diagnostic output for
1027 // struct/union/array/enum
1028 if(old_type.id()==ID_struct ||
1029 old_type.id()==ID_union ||
1030 old_type.id()==ID_array ||
1031 old_type.id()==ID_c_enum)
1033 old_symbol,
1034 new_symbol,
1035 old_symbol.type,
1036 new_symbol.type);
1037
1038 link_error(
1039 old_symbol,
1040 new_symbol,
1041 "conflicting types for variable");
1042
1043 // error logged, continue typechecking other symbols
1044 return;
1045 }
1046 else if(set_to_new)
1047 old_symbol.type=new_symbol.type;
1048
1050 old_symbol.symbol_expr(), old_symbol.symbol_expr());
1051 }
1052
1053 // care about initializers
1054
1055 if(!new_symbol.value.is_nil())
1056 {
1057 if(old_symbol.value.is_nil() ||
1058 old_symbol.is_weak)
1059 {
1060 // new_symbol wins
1061 old_symbol.value=new_symbol.value;
1062 old_symbol.is_macro=new_symbol.is_macro;
1063 }
1064 else if(!new_symbol.is_weak)
1065 {
1066 // try simplifier
1067 exprt tmp_old=old_symbol.value,
1068 tmp_new=new_symbol.value;
1069
1070 simplify(tmp_old, ns);
1071 simplify(tmp_new, ns);
1072
1073 if(base_type_eq(tmp_old, tmp_new, ns))
1074 {
1075 // ok, the same
1076 }
1077 else
1078 {
1079 warning().source_location=new_symbol.location;
1080
1081 warning() << "warning: conflicting initializers for"
1082 << " variable \"" << old_symbol.name << "\"\n";
1083 warning() << "using old value in module " << old_symbol.module << " "
1084 << old_symbol.value.find_source_location() << '\n'
1085 << expr_to_string(old_symbol.name, tmp_old) << '\n';
1086 warning() << "ignoring new value in module " << new_symbol.module << " "
1087 << new_symbol.value.find_source_location() << '\n'
1088 << expr_to_string(new_symbol.name, tmp_new) << eom;
1089 }
1090 }
1091 }
1092 else if(set_to_new && !old_symbol.value.is_nil())
1093 {
1094 // the type has been updated, now make sure that the initialising assignment
1095 // will have matching types
1096 old_symbol.value = typecast_exprt(old_symbol.value, old_symbol.type);
1097 }
1098}
1099
1101 symbolt &old_symbol,
1102 symbolt &new_symbol)
1103{
1104 // see if it is a function or a variable
1105
1106 bool is_code_old_symbol=old_symbol.type.id()==ID_code;
1107 bool is_code_new_symbol=new_symbol.type.id()==ID_code;
1108
1109 if(is_code_old_symbol!=is_code_new_symbol)
1110 {
1111 link_error(
1112 old_symbol,
1113 new_symbol,
1114 "conflicting definition for symbol");
1115
1116 // error logged, continue typechecking other symbols
1117 return;
1118 }
1119
1120 if(is_code_old_symbol)
1121 duplicate_code_symbol(old_symbol, new_symbol);
1122 else
1123 duplicate_object_symbol(old_symbol, new_symbol);
1124
1125 // care about flags
1126
1127 if(old_symbol.is_extern && !new_symbol.is_extern)
1128 old_symbol.location=new_symbol.location;
1129
1130 // it's enough that one isn't extern for the final one not to be
1131 old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
1132}
1133
1135 symbolt &old_symbol,
1136 const symbolt &new_symbol)
1137{
1138 assert(new_symbol.is_type);
1139
1140 if(!old_symbol.is_type)
1141 {
1142 link_error(
1143 old_symbol,
1144 new_symbol,
1145 "conflicting definition for symbol");
1146
1147 // error logged, continue typechecking other symbols
1148 return;
1149 }
1150
1151 if(old_symbol.type==new_symbol.type)
1152 return;
1153
1154 if(
1155 old_symbol.type.id() == ID_struct &&
1156 to_struct_type(old_symbol.type).is_incomplete() &&
1157 new_symbol.type.id() == ID_struct &&
1158 !to_struct_type(new_symbol.type).is_incomplete())
1159 {
1160 old_symbol.type=new_symbol.type;
1161 old_symbol.location=new_symbol.location;
1162 return;
1163 }
1164
1165 if(
1166 old_symbol.type.id() == ID_struct &&
1167 !to_struct_type(old_symbol.type).is_incomplete() &&
1168 new_symbol.type.id() == ID_struct &&
1169 to_struct_type(new_symbol.type).is_incomplete())
1170 {
1171 // ok, keep old
1172 return;
1173 }
1174
1175 if(
1176 old_symbol.type.id() == ID_union &&
1177 to_union_type(old_symbol.type).is_incomplete() &&
1178 new_symbol.type.id() == ID_union &&
1179 !to_union_type(new_symbol.type).is_incomplete())
1180 {
1181 old_symbol.type=new_symbol.type;
1182 old_symbol.location=new_symbol.location;
1183 return;
1184 }
1185
1186 if(
1187 old_symbol.type.id() == ID_union &&
1188 !to_union_type(old_symbol.type).is_incomplete() &&
1189 new_symbol.type.id() == ID_union &&
1190 to_union_type(new_symbol.type).is_incomplete())
1191 {
1192 // ok, keep old
1193 return;
1194 }
1195
1196 if(
1197 old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array &&
1199 to_array_type(old_symbol.type).element_type(),
1200 to_array_type(new_symbol.type).element_type(),
1201 ns))
1202 {
1203 if(to_array_type(old_symbol.type).size().is_nil() &&
1204 to_array_type(new_symbol.type).size().is_not_nil())
1205 {
1206 to_array_type(old_symbol.type).size()=
1207 to_array_type(new_symbol.type).size();
1208 return;
1209 }
1210
1211 if(to_array_type(new_symbol.type).size().is_nil() &&
1212 to_array_type(old_symbol.type).size().is_not_nil())
1213 {
1214 // ok, keep old
1215 return;
1216 }
1217 }
1218
1220 old_symbol,
1221 new_symbol,
1222 old_symbol.type,
1223 new_symbol.type);
1224
1225 link_error(
1226 old_symbol,
1227 new_symbol,
1228 "unexpected difference between type symbols");
1229}
1230
1232 const symbolt &old_symbol,
1233 const symbolt &new_symbol)
1234{
1235 assert(new_symbol.is_type);
1236
1237 if(!old_symbol.is_type)
1238 return true;
1239
1240 if(old_symbol.type==new_symbol.type)
1241 return false;
1242
1243 if(
1244 old_symbol.type.id() == ID_struct &&
1245 to_struct_type(old_symbol.type).is_incomplete() &&
1246 new_symbol.type.id() == ID_struct &&
1247 !to_struct_type(new_symbol.type).is_incomplete())
1248 return false; // not different
1249
1250 if(
1251 old_symbol.type.id() == ID_struct &&
1252 !to_struct_type(old_symbol.type).is_incomplete() &&
1253 new_symbol.type.id() == ID_struct &&
1254 to_struct_type(new_symbol.type).is_incomplete())
1255 return false; // not different
1256
1257 if(
1258 old_symbol.type.id() == ID_union &&
1259 to_union_type(old_symbol.type).is_incomplete() &&
1260 new_symbol.type.id() == ID_union &&
1261 !to_union_type(new_symbol.type).is_incomplete())
1262 return false; // not different
1263
1264 if(
1265 old_symbol.type.id() == ID_union &&
1266 !to_union_type(old_symbol.type).is_incomplete() &&
1267 new_symbol.type.id() == ID_union &&
1268 to_union_type(new_symbol.type).is_incomplete())
1269 return false; // not different
1270
1271 if(
1272 old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array &&
1274 to_array_type(old_symbol.type).element_type(),
1275 to_array_type(new_symbol.type).element_type(),
1276 ns))
1277 {
1278 if(to_array_type(old_symbol.type).size().is_nil() &&
1279 to_array_type(new_symbol.type).size().is_not_nil())
1280 return false; // not different
1281
1282 if(to_array_type(new_symbol.type).size().is_nil() &&
1283 to_array_type(old_symbol.type).size().is_not_nil())
1284 return false; // not different
1285 }
1286
1287 return true; // different
1288}
1289
1291 std::unordered_set<irep_idt> &needs_to_be_renamed)
1292{
1293 // Any type that uses a symbol that will be renamed also
1294 // needs to be renamed, and so on, until saturation.
1295
1296 used_byt used_by;
1297
1298 for(const auto &symbol_pair : src_symbol_table.symbols)
1299 {
1300 if(symbol_pair.second.is_type)
1301 {
1302 // find type and array-size symbols
1303 find_symbols_sett symbols_used;
1304 find_type_and_expr_symbols(symbol_pair.second.type, symbols_used);
1305
1306 for(const auto &symbol_used : symbols_used)
1307 {
1308 used_by[symbol_used].insert(symbol_pair.first);
1309 }
1310 }
1311 }
1312
1313 std::deque<irep_idt> queue(
1314 needs_to_be_renamed.begin(), needs_to_be_renamed.end());
1315
1316 while(!queue.empty())
1317 {
1318 irep_idt id = queue.back();
1319 queue.pop_back();
1320
1321 const std::unordered_set<irep_idt> &u = used_by[id];
1322
1323 for(const auto &dep : u)
1324 if(needs_to_be_renamed.insert(dep).second)
1325 {
1326 queue.push_back(dep);
1327 #ifdef DEBUG
1328 debug() << "LINKING: needs to be renamed (dependency): "
1329 << dep << eom;
1330 #endif
1331 }
1332 }
1333}
1334
1335std::unordered_map<irep_idt, irep_idt> linkingt::rename_symbols(
1336 const std::unordered_set<irep_idt> &needs_to_be_renamed)
1337{
1338 std::unordered_map<irep_idt, irep_idt> new_identifiers;
1340
1341 for(const irep_idt &id : needs_to_be_renamed)
1342 {
1343 const symbolt &new_symbol = src_ns.lookup(id);
1344
1345 irep_idt new_identifier;
1346
1347 if(new_symbol.is_type)
1348 new_identifier=type_to_name(src_ns, id, new_symbol.type);
1349 else
1350 new_identifier=rename(id);
1351
1352 new_identifiers.emplace(id, new_identifier);
1353
1354#ifdef DEBUG
1355 debug() << "LINKING: renaming " << id << " to "
1356 << new_identifier << eom;
1357#endif
1358
1359 if(new_symbol.is_type)
1360 rename_symbol.insert_type(id, new_identifier);
1361 else
1362 rename_symbol.insert_expr(id, new_identifier);
1363 }
1364
1365 return new_identifiers;
1366}
1367
1369 const std::unordered_map<irep_idt, irep_idt> &new_identifiers)
1370{
1371 std::map<irep_idt, symbolt> src_symbols;
1372 // First apply the renaming
1373 for(const auto &named_symbol : src_symbol_table.symbols)
1374 {
1375 symbolt symbol=named_symbol.second;
1376 // apply the renaming
1377 rename_symbol(symbol.type);
1378 rename_symbol(symbol.value);
1379 auto it = new_identifiers.find(named_symbol.first);
1380 if(it != new_identifiers.end())
1381 symbol.name = it->second;
1382
1383 src_symbols.emplace(named_symbol.first, std::move(symbol));
1384 }
1385
1386 // Move over all the non-colliding ones
1387 std::unordered_set<irep_idt> collisions;
1388
1389 for(const auto &named_symbol : src_symbols)
1390 {
1391 // renamed?
1392 if(named_symbol.first!=named_symbol.second.name)
1393 {
1394 // new
1395 main_symbol_table.add(named_symbol.second);
1396 }
1397 else
1398 {
1399 if(!main_symbol_table.has_symbol(named_symbol.first))
1400 {
1401 // new
1402 main_symbol_table.add(named_symbol.second);
1403 }
1404 else
1405 collisions.insert(named_symbol.first);
1406 }
1407 }
1408
1409 // Now do the collisions
1410 for(const irep_idt &collision : collisions)
1411 {
1412 symbolt &old_symbol = main_symbol_table.get_writeable_ref(collision);
1413 symbolt &new_symbol=src_symbols.at(collision);
1414
1415 if(new_symbol.is_type)
1416 duplicate_type_symbol(old_symbol, new_symbol);
1417 else
1418 duplicate_non_type_symbol(old_symbol, new_symbol);
1419 }
1420
1421 // Apply type updates to initializers
1422 for(const auto &named_symbol : main_symbol_table.symbols)
1423 {
1424 if(!named_symbol.second.is_type &&
1425 !named_symbol.second.is_macro &&
1426 named_symbol.second.value.is_not_nil())
1427 {
1429 main_symbol_table.get_writeable_ref(named_symbol.first).value);
1430 }
1431 }
1432}
1433
1435{
1436 // We do this in three phases. We first figure out which symbols need to
1437 // be renamed, and then build the renaming, and finally apply this
1438 // renaming in the second pass over the symbol table.
1439
1440 // PHASE 1: identify symbols to be renamed
1441
1442 std::unordered_set<irep_idt> needs_to_be_renamed;
1443
1444 for(const auto &symbol_pair : src_symbol_table.symbols)
1445 {
1446 symbol_tablet::symbolst::const_iterator m_it =
1447 main_symbol_table.symbols.find(symbol_pair.first);
1448
1449 if(
1450 m_it != main_symbol_table.symbols.end() && // duplicate
1451 needs_renaming(m_it->second, symbol_pair.second))
1452 {
1453 needs_to_be_renamed.insert(symbol_pair.first);
1454 #ifdef DEBUG
1455 debug() << "LINKING: needs to be renamed: " << symbol_pair.first << eom;
1456 #endif
1457 }
1458 }
1459
1460 // renaming types may trigger further renaming
1461 do_type_dependencies(needs_to_be_renamed);
1462
1463 // PHASE 2: actually rename them
1464 auto new_identifiers = rename_symbols(needs_to_be_renamed);
1465
1466 // PHASE 3: copy new symbols to main table
1467 copy_symbols(new_identifiers);
1468}
1469
1471 symbol_tablet &dest_symbol_table,
1472 const symbol_tablet &new_symbol_table,
1473 message_handlert &message_handler)
1474{
1476 dest_symbol_table, new_symbol_table, message_handler);
1477
1478 return linking.typecheck_main();
1479}
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:291
Base Type Computation.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
const memberst & members() const
Definition: c_types.h:255
std::vector< c_enum_membert > memberst
Definition: c_types.h:253
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: linking.cpp:30
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
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
bool has_ellipsis() const
Definition: std_types.h:611
A constant literal expression.
Definition: std_expr.h:2807
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
Unbounded, signed integers (mathematical integers, not bitvectors)
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
bool is_not_nil() const
Definition: irep.h:380
const std::string & id_string() const
Definition: irep.h:399
void make_nil()
Definition: irep.h:454
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1100
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition: linking.cpp:995
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1231
rename_symbolt rename_symbol
Definition: linking_class.h:44
void copy_symbols(const std::unordered_map< irep_idt, irep_idt > &)
Definition: linking.cpp:1368
namespacet ns
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition: linking.cpp:814
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:459
virtual void typecheck()
Definition: linking.cpp:1434
std::unordered_map< irep_idt, irep_idt > rename_symbols(const std::unordered_set< irep_idt > &needs_to_be_renamed)
Definition: linking.cpp:1335
irep_idt rename(const irep_idt &)
Definition: linking.cpp:435
symbol_table_baset & main_symbol_table
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > used_byt
std::string expr_to_string(const irep_idt &identifier, const exprt &expr) const
Definition: linking.cpp:50
void detailed_conflict_report_rec(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2, unsigned depth, exprt &conflict_path)
Definition: linking.cpp:130
void do_type_dependencies(std::unordered_set< irep_idt > &)
Definition: linking.cpp:1290
const symbol_table_baset & src_symbol_table
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:417
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1010
casting_replace_symbolt object_type_updates
Definition: linking_class.h:45
std::string type_to_string(const irep_idt &identifier, const typet &type) const
Definition: linking.cpp:57
std::unordered_set< irep_idt > renamed_ids
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1134
std::string type_to_string_verbose(const symbolt &symbol, const typet &type) const
Definition: linking.cpp:78
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking_class.h:56
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:473
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:400
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & compound() const
Definition: std_expr.h:2708
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & debug() const
Definition: message.h:429
mstreamt & warning() const
Definition: message.h:404
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:40
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
expr_mapt expr_map
std::string as_string() const
const componentst & components() const
Definition: std_types.h:147
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:185
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:99
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
bool is_extern
Definition: symbol.h:66
bool is_macro
Definition: symbol.h:61
bool is_file_local
Definition: symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
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
bool is_weak
Definition: symbol.h:67
irep_idt name
The unique identifier.
Definition: symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
exprt value
Initial value of symbol.
Definition: symbol.h:34
const irep_idt & get_identifier() const
Definition: std_types.h:410
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const source_locationt & source_location() const
Definition: type.h:74
The union type.
Definition: c_types.h:125
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:23
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool linking(symbol_tablet &dest_symbol_table, const symbol_tablet &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition: linking.cpp:1470
static const typet & follow_tags_symbols(const namespacet &ns, const typet &type)
Definition: linking.cpp:64
ANSI-C Linking.
ANSI-C Linking.
bool is_true(const literalt &l)
Definition: literal.h:198
Mathematical types.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
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
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:434
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::unordered_set< irep_idt > o_symbols
std::unordered_set< irep_idt > n_symbols
Author: Diffblue Ltd.
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177