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