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