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