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