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