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