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