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