cprover
dump_c.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dump Goto-Program as C/C++ Source
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "dump_c.h"
13 
14 #include <util/byte_operators.h>
15 #include <util/config.h>
16 #include <util/expr_initializer.h>
17 #include <util/find_symbols.h>
18 #include <util/get_base_name.h>
19 #include <util/invariant.h>
20 #include <util/replace_symbol.h>
21 #include <util/string_utils.h>
22 
23 #include <ansi-c/expr2c.h>
24 #include <cpp/expr2cpp.h>
25 
27 
28 #include "dump_c_class.h"
29 #include "goto_program2code.h"
30 
33 
40 
41 inline std::ostream &operator << (std::ostream &out, dump_ct &src)
42 {
43  src(out);
44  return out;
45 }
46 
47 void dump_ct::operator()(std::ostream &os)
48 {
49  std::stringstream func_decl_stream;
50  std::stringstream compound_body_stream;
51  std::stringstream global_var_stream;
52  std::stringstream global_decl_stream;
53  std::stringstream global_decl_header_stream;
54  std::stringstream func_body_stream;
55  local_static_declst local_static_decls;
56 
57  // add copies of struct types when ID_C_transparent_union is only
58  // annotated to parameter
59  symbol_tablet symbols_transparent;
60  for(const auto &named_symbol : copied_symbol_table.symbols)
61  {
62  const symbolt &symbol=named_symbol.second;
63 
64  if(symbol.type.id()!=ID_code)
65  continue;
66 
67  code_typet &code_type=to_code_type(
68  copied_symbol_table.get_writeable_ref(named_symbol.first).type);
69  code_typet::parameterst &parameters=code_type.parameters();
70 
71  for(code_typet::parameterst::iterator
72  it2=parameters.begin();
73  it2!=parameters.end();
74  ++it2)
75  {
76  typet &type=it2->type();
77 
78  if(type.id() == ID_union_tag && type.get_bool(ID_C_transparent_union))
79  {
80  symbolt new_type_sym =
81  ns.lookup(to_union_tag_type(type).get_identifier());
82 
83  new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
84  new_type_sym.type.set(ID_C_transparent_union, true);
85 
86  // we might have it already, in which case this has no effect
87  symbols_transparent.add(new_type_sym);
88 
89  to_union_tag_type(type).set_identifier(new_type_sym.name);
90  type.remove(ID_C_transparent_union);
91  }
92  }
93  }
94  for(const auto &symbol_pair : symbols_transparent.symbols)
95  {
96  copied_symbol_table.add(symbol_pair.second);
97  }
98 
99  typedef std::unordered_map<irep_idt, unsigned> unique_tagst;
100  unique_tagst unique_tags;
101 
102  // add tags to anonymous union/struct/enum,
103  // and prepare lexicographic order
104  std::set<std::string> symbols_sorted;
105  for(const auto &named_symbol : copied_symbol_table.symbols)
106  {
107  symbolt &symbol = copied_symbol_table.get_writeable_ref(named_symbol.first);
108  bool tag_added=false;
109 
110  // TODO we could get rid of some of the ID_anonymous by looking up
111  // the origin symbol types in typedef_types and adjusting any other
112  // uses of ID_tag
113  if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
114  symbol.type.get(ID_tag).empty())
115  {
116  PRECONDITION(symbol.is_type);
117  symbol.type.set(ID_tag, ID_anonymous);
118  tag_added=true;
119  }
120  else if(symbol.type.id()==ID_c_enum &&
121  symbol.type.find(ID_tag).get(ID_C_base_name).empty())
122  {
123  PRECONDITION(symbol.is_type);
124  symbol.type.add(ID_tag).set(ID_C_base_name, ID_anonymous);
125  tag_added=true;
126  }
127 
128  const std::string name_str=id2string(named_symbol.first);
129  if(symbol.is_type &&
130  (symbol.type.id()==ID_union ||
131  symbol.type.id()==ID_struct ||
132  symbol.type.id()==ID_c_enum))
133  {
134  std::string new_tag=symbol.type.id()==ID_c_enum?
135  symbol.type.find(ID_tag).get_string(ID_C_base_name):
136  symbol.type.get_string(ID_tag);
137 
138  std::string::size_type tag_pos=new_tag.rfind("tag-");
139  if(tag_pos!=std::string::npos)
140  new_tag.erase(0, tag_pos+4);
141  const std::string new_tag_base=new_tag;
142 
143  for(std::pair<unique_tagst::iterator, bool>
144  unique_entry=unique_tags.insert(std::make_pair(new_tag, 0));
145  !unique_entry.second;
146  unique_entry=unique_tags.insert(std::make_pair(new_tag, 0)))
147  {
148  new_tag=new_tag_base+"$"+
149  std::to_string(unique_entry.first->second);
150  ++(unique_entry.first->second);
151  }
152 
153  if(symbol.type.id()==ID_c_enum)
154  {
155  symbol.type.add(ID_tag).set(ID_C_base_name, new_tag);
156  symbol.base_name=new_tag;
157  }
158  else
159  symbol.type.set(ID_tag, new_tag);
160  }
161 
162  // we don't want to dump in full all definitions; in particular
163  // do not dump anonymous types that are defined in system headers
164  if((!tag_added || symbol.is_type) &&
166  symbol.name!=goto_functions.entry_point())
167  continue;
168 
169  bool inserted=symbols_sorted.insert(name_str).second;
170  CHECK_RETURN(inserted);
171  }
172 
174 
175  // collect all declarations we might need, include local static variables
176  bool skip_function_main=false;
177  std::vector<std::string> header_files;
178  for(std::set<std::string>::const_iterator
179  it=symbols_sorted.begin();
180  it!=symbols_sorted.end();
181  ++it)
182  {
183  const symbolt &symbol=ns.lookup(*it);
184  const irep_idt &type_id=symbol.type.id();
185 
186  if(symbol.is_type &&
187  symbol.location.get_function().empty() &&
188  (type_id==ID_struct ||
189  type_id==ID_union ||
190  type_id==ID_c_enum))
191  {
193  {
194  global_decl_stream << "// " << symbol.name << '\n';
195  global_decl_stream << "// " << symbol.location << '\n';
196 
197  std::string location_file =
198  get_base_name(id2string(symbol.location.get_file()), false);
199  // collect header the types are borrowed from
200  // expect header files to end in .h
201  if(
202  location_file.length() > 1 &&
203  location_file[location_file.length() - 1] == 'h')
204  {
205  std::vector<std::string>::iterator it =
206  find(header_files.begin(), header_files.end(), location_file);
207  if(it == header_files.end())
208  {
209  header_files.push_back(location_file);
210  global_decl_header_stream << "#include \"" << location_file
211  << "\"\n";
212  }
213  }
214 
215  if(type_id==ID_c_enum)
216  convert_compound_enum(symbol.type, global_decl_stream);
217  else if(type_id == ID_struct)
218  {
219  global_decl_stream << type_to_string(struct_tag_typet{symbol.name})
220  << ";\n\n";
221  }
222  else
223  {
224  global_decl_stream << type_to_string(union_tag_typet{symbol.name})
225  << ";\n\n";
226  }
227  }
228  }
229  else if(
230  symbol.is_static_lifetime && symbol.type.id() != ID_code &&
231  !symbol.type.get_bool(ID_C_do_not_dump))
233  symbol,
234  global_var_stream,
235  local_static_decls);
236  else if(symbol.type.id()==ID_code)
237  {
238  goto_functionst::function_mapt::const_iterator func_entry=
239  goto_functions.function_map.find(symbol.name);
240 
241  if(
242  !harness && func_entry != goto_functions.function_map.end() &&
243  func_entry->second.body_available() &&
244  (symbol.name == ID_main ||
245  (config.main.has_value() && symbol.name == config.main.value())))
246  {
247  skip_function_main=true;
248  }
249  }
250  }
251 
252  // function declarations and definitions
253  for(std::set<std::string>::const_iterator
254  it=symbols_sorted.begin();
255  it!=symbols_sorted.end();
256  ++it)
257  {
258  const symbolt &symbol=ns.lookup(*it);
259 
260  if(symbol.type.id()!=ID_code ||
261  symbol.is_type)
262  continue;
263 
265  symbol,
266  skip_function_main,
267  func_decl_stream,
268  func_body_stream,
269  local_static_decls);
270  }
271 
272  // (possibly modified) compound types
273  for(std::set<std::string>::const_iterator
274  it=symbols_sorted.begin();
275  it!=symbols_sorted.end();
276  ++it)
277  {
278  const symbolt &symbol=ns.lookup(*it);
279 
280  if(
281  symbol.is_type &&
282  (symbol.type.id() == ID_struct || symbol.type.id() == ID_union))
284  symbol,
285  compound_body_stream);
286  }
287 
288  // Dump the code to the target stream;
289  // the statements before to this point collect the code to dump!
290  for(std::set<std::string>::const_iterator
291  it=system_headers.begin();
292  it!=system_headers.end();
293  ++it)
294  os << "#include <" << *it << ">\n";
295  if(!system_headers.empty())
296  os << '\n';
297 
298  if(!global_decl_header_stream.str().empty() && dump_c_config.include_headers)
299  os << global_decl_header_stream.str() << '\n';
300 
301  if(global_var_stream.str().find("NULL")!=std::string::npos ||
302  func_body_stream.str().find("NULL")!=std::string::npos)
303  {
304  os << "#ifndef NULL\n"
305  << "#define NULL ((void*)0)\n"
306  << "#endif\n\n";
307  }
308  if(func_body_stream.str().find("FENCE")!=std::string::npos)
309  {
310  os << "#ifndef FENCE\n"
311  << "#define FENCE(x) ((void)0)\n"
312  << "#endif\n\n";
313  }
314  if(func_body_stream.str().find("IEEE_FLOAT_")!=std::string::npos)
315  {
316  os << "#ifndef IEEE_FLOAT_EQUAL\n"
317  << "#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n"
318  << "#endif\n"
319  << "#ifndef IEEE_FLOAT_NOTEQUAL\n"
320  << "#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n"
321  << "#endif\n\n";
322  }
323 
324  if(!global_decl_stream.str().empty() && dump_c_config.include_global_decls)
325  os << global_decl_stream.str() << '\n';
326 
328  dump_typedefs(os);
329 
330  if(!func_decl_stream.str().empty() && dump_c_config.include_function_decls)
331  os << func_decl_stream.str() << '\n';
332  if(!compound_body_stream.str().empty() && dump_c_config.include_compounds)
333  os << compound_body_stream.str() << '\n';
334  if(!global_var_stream.str().empty() && dump_c_config.include_global_vars)
335  os << global_var_stream.str() << '\n';
337  os << func_body_stream.str();
338 }
339 
342  const symbolt &symbol,
343  std::ostream &os_body)
344 {
345  if(
346  !symbol.location.get_function().empty() ||
347  symbol.type.get_bool(ID_C_do_not_dump))
348  {
349  return;
350  }
351 
352  // do compound type body
353  if(symbol.type.id() == ID_struct)
355  symbol.type,
356  struct_tag_typet(symbol.name),
358  os_body);
359  else if(symbol.type.id() == ID_union)
361  symbol.type,
362  union_tag_typet(symbol.name),
364  os_body);
365  else if(symbol.type.id() == ID_c_enum)
367  symbol.type,
368  c_enum_tag_typet(symbol.name),
370  os_body);
371 }
372 
374  const typet &type,
375  const typet &unresolved,
376  bool recursive,
377  std::ostream &os)
378 {
379  if(
380  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
381  type.id() == ID_union_tag)
382  {
383  const symbolt &symbol = ns.lookup(to_tag_type(type));
384  DATA_INVARIANT(symbol.is_type, "tag expected to be type symbol");
385 
387  convert_compound(symbol.type, unresolved, recursive, os);
388  }
389  else if(type.id()==ID_array || type.id()==ID_pointer)
390  {
391  if(!recursive)
392  return;
393 
394  convert_compound(type.subtype(), type.subtype(), recursive, os);
395 
396  // sizeof may contain a type symbol that has to be declared first
397  if(type.id()==ID_array)
398  {
399  find_symbols_sett syms;
400  find_non_pointer_type_symbols(to_array_type(type).size(), syms);
401 
402  for(find_symbols_sett::const_iterator
403  it=syms.begin();
404  it!=syms.end();
405  ++it)
406  {
407  const symbolt &type_symbol = ns.lookup(*it);
408  irep_idt tag_kind =
409  type_symbol.type.id() == ID_c_enum
410  ? ID_c_enum_tag
411  : (type_symbol.type.id() == ID_union ? ID_union_tag
412  : ID_struct_tag);
413  tag_typet s_type(tag_kind, *it);
414  convert_compound(s_type, s_type, recursive, os);
415  }
416  }
417  }
418  else if(type.id()==ID_struct || type.id()==ID_union)
419  convert_compound(to_struct_union_type(type), unresolved, recursive, os);
420  else if(type.id()==ID_c_enum)
421  convert_compound_enum(type, os);
422 }
423 
425  const struct_union_typet &type,
426  const typet &unresolved,
427  bool recursive,
428  std::ostream &os)
429 {
430  const irep_idt &name=type.get(ID_tag);
431 
432  if(!converted_compound.insert(name).second || type.get_bool(ID_C_do_not_dump))
433  return;
434 
435  // make sure typedef names used in the declaration are available
436  collect_typedefs(type, true);
437 
438  const irept &bases = type.find(ID_bases);
439  std::stringstream base_decls;
440  for(const auto &parent : bases.get_sub())
441  {
442  UNREACHABLE;
443  (void)parent;
444 #if 0
445  assert(parent.id() == ID_base);
446  assert(parent.get(ID_type) == ID_struct_tag);
447 
448  const irep_idt &base_id=
449  parent.find(ID_type).get(ID_identifier);
450  const irep_idt &renamed_base_id=global_renaming[base_id];
451  const symbolt &parsymb=ns.lookup(renamed_base_id);
452 
453  convert_compound_rec(parsymb.type, os);
454 
455  base_decls << id2string(renamed_base_id) +
456  (parent_it+1==bases.get_sub().end()?"":", ");
457 #endif
458  }
459 
460 #if 0
461  // for the constructor
462  string constructor_args;
463  string constructor_body;
464 
465  std::string component_name = id2string(renaming[compo.get(ID_name)]);
466  assert(component_name != "");
467 
468  if(it != struct_type.components().begin()) constructor_args += ", ";
469 
470  if(compo.type().id() == ID_pointer)
471  constructor_args += type_to_string(compo.type()) + component_name;
472  else
473  constructor_args += "const " + type_to_string(compo.type()) + "& " + component_name;
474 
475  constructor_body += indent + indent + "this->"+component_name + " = " + component_name + ";\n";
476 #endif
477 
478  std::stringstream struct_body;
479 
480  for(const auto &comp : type.components())
481  {
482  const typet &comp_type = comp.type();
483 
484  if(comp_type.id()==ID_code ||
485  comp.get_bool(ID_from_base) ||
486  comp.get_is_padding())
487  continue;
488 
489  const typet *non_array_type = &comp_type;
490  while(non_array_type->id()==ID_array)
491  non_array_type = &(non_array_type->subtype());
492 
493  if(recursive)
494  {
495  if(non_array_type->id()!=ID_pointer)
496  convert_compound(comp.type(), comp.type(), recursive, os);
497  else
498  collect_typedefs(comp.type(), true);
499  }
500 
501  irep_idt comp_name=comp.get_name();
502 
503  struct_body << indent(1) << "// " << comp_name << '\n';
504  struct_body << indent(1);
505 
506  // component names such as "main" would collide with other objects in the
507  // namespace
508  std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
509  std::string s=make_decl(fake_unique_name, comp.type());
510  POSTCONDITION(s.find("NO/SUCH/NS")==std::string::npos);
511 
512  if(comp_type.id()==ID_c_bit_field &&
513  to_c_bit_field_type(comp_type).get_width()==0)
514  {
515  comp_name.clear();
516  s=type_to_string(comp_type);
517  }
518 
519  if(s.find(CPROVER_PREFIX "bitvector") == std::string::npos)
520  {
521  struct_body << s;
522  }
523  else if(comp_type.id()==ID_signedbv)
524  {
525  const signedbv_typet &t=to_signedbv_type(comp_type);
527  struct_body << "long long int " << comp_name
528  << " : " << t.get_width();
529  else if(mode == ID_cpp)
530  struct_body << "__signedbv<" << t.get_width() << "> "
531  << comp_name;
532  else
533  struct_body << s;
534  }
535  else if(comp_type.id()==ID_unsignedbv)
536  {
537  const unsignedbv_typet &t=to_unsignedbv_type(comp_type);
539  struct_body << "unsigned long long " << comp_name
540  << " : " << t.get_width();
541  else if(mode == ID_cpp)
542  struct_body << "__unsignedbv<" << t.get_width() << "> "
543  << comp_name;
544  else
545  struct_body << s;
546  }
547  else
548  UNREACHABLE;
549 
550  struct_body << ";\n";
551  }
552 
553  typet unresolved_clean=unresolved;
554  irep_idt typedef_str;
555  for(auto td_entry : typedef_types)
556  {
557  if(
558  td_entry.first.get(ID_identifier) == unresolved.get(ID_identifier) &&
559  (td_entry.first.source_location() == unresolved.source_location()))
560  {
561  unresolved_clean.remove(ID_C_typedef);
562  typedef_str = td_entry.second;
563  std::pair<typedef_mapt::iterator, bool> td_map_entry =
564  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
565  PRECONDITION(!td_map_entry.second);
566  if(!td_map_entry.first->second.early)
567  td_map_entry.first->second.type_decl_str.clear();
568  os << "typedef ";
569  break;
570  }
571  }
572 
573  os << type_to_string(unresolved_clean);
574  if(!base_decls.str().empty())
575  {
576  PRECONDITION(mode == ID_cpp);
577  os << ": " << base_decls.str();
578  }
579  os << '\n';
580  os << "{\n";
581  os << struct_body.str();
582 
583  /*
584  if(!struct_type.components().empty())
585  {
586  os << indent << name << "(){}\n";
587  os << indent << "explicit " << name
588  << "(" + constructor_args + ")\n";
589  os << indent << "{\n";
590  os << constructor_body;
591  os << indent << "}\n";
592  }
593  */
594 
595  os << "}";
596  if(type.get_bool(ID_C_transparent_union))
597  os << " __attribute__ ((__transparent_union__))";
598  if(type.get_bool(ID_C_packed))
599  os << " __attribute__ ((__packed__))";
600  if(!typedef_str.empty())
601  os << " " << typedef_str;
602  os << ";\n\n";
603 }
604 
606  const typet &type,
607  std::ostream &os)
608 {
609  PRECONDITION(type.id()==ID_c_enum);
610 
611  const irept &tag=type.find(ID_tag);
612  const irep_idt &name=tag.get(ID_C_base_name);
613 
614  if(tag.is_nil() ||
615  !converted_enum.insert(name).second)
616  return;
617 
618  c_enum_typet enum_type=to_c_enum_type(type);
619  c_enum_typet::memberst &members=
620  (c_enum_typet::memberst &)(enum_type.add(ID_body).get_sub());
621  for(c_enum_typet::memberst::iterator
622  it=members.begin();
623  it!=members.end();
624  ++it)
625  {
626  const irep_idt bn=it->get_base_name();
627 
628  if(declared_enum_constants.find(bn)!=
629  declared_enum_constants.end() ||
631  {
632  std::string new_bn=id2string(name)+"$$"+id2string(bn);
633  it->set_base_name(new_bn);
634  }
635 
637  std::make_pair(bn, it->get_base_name()));
638  }
639 
640  os << type_to_string(enum_type);
641 
642  if(enum_type.get_bool(ID_C_packed))
643  os << " __attribute__ ((__packed__))";
644 
645  os << ";\n\n";
646 }
647 
649  code_declt &decl,
650  std::list<irep_idt> &local_static,
651  std::list<irep_idt> &local_type_decls)
652 {
653  goto_programt tmp;
654  tmp.add(goto_programt::make_decl(decl.symbol()));
655 
656  if(optionalt<exprt> value = decl.initial_value())
657  {
658  decl.set_initial_value({});
659  tmp.add(goto_programt::make_assignment(decl.symbol(), std::move(*value)));
660  }
661 
663 
664  // goto_program2codet requires valid location numbers:
665  tmp.update();
666 
667  std::unordered_set<irep_idt> typedef_names;
668  for(const auto &td : typedef_map)
669  typedef_names.insert(td.first);
670 
671  code_blockt b;
672  goto_program2codet p2s(
673  irep_idt(),
674  tmp,
676  b,
677  local_static,
678  local_type_decls,
679  typedef_names,
681  p2s();
682 
683  POSTCONDITION(b.statements().size() == 1);
684  decl.swap(b.op0());
685 }
686 
692 void dump_ct::collect_typedefs(const typet &type, bool early)
693 {
694  std::unordered_set<irep_idt> deps;
695  collect_typedefs_rec(type, early, deps);
696 }
697 
706  const typet &type,
707  bool early,
708  std::unordered_set<irep_idt> &dependencies)
709 {
711  return;
712 
713  std::unordered_set<irep_idt> local_deps;
714 
715  if(type.id()==ID_code)
716  {
717  const code_typet &code_type=to_code_type(type);
718 
719  collect_typedefs_rec(code_type.return_type(), early, local_deps);
720  for(const auto &param : code_type.parameters())
721  collect_typedefs_rec(param.type(), early, local_deps);
722  }
723  else if(type.id()==ID_pointer || type.id()==ID_array)
724  {
725  collect_typedefs_rec(type.subtype(), early, local_deps);
726  }
727  else if(
728  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
729  type.id() == ID_union_tag)
730  {
731  const symbolt &symbol = ns.lookup(to_tag_type(type));
732  collect_typedefs_rec(symbol.type, early, local_deps);
733  }
734 
735  const irep_idt &typedef_str=type.get(ID_C_typedef);
736 
737  if(!typedef_str.empty())
738  {
739  std::pair<typedef_mapt::iterator, bool> entry=
740  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
741 
742  if(entry.second ||
743  (early && entry.first->second.type_decl_str.empty()))
744  {
745  if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
746  {
747  system_headers.insert("stdarg.h");
748  early=false;
749  }
750  else
751  {
752  typet t=type;
753  t.remove(ID_C_typedef);
754 
755  std::ostringstream oss;
756  oss << "typedef " << make_decl(typedef_str, t) << ';';
757 
758  entry.first->second.type_decl_str=oss.str();
759  entry.first->second.dependencies=local_deps;
760  }
761  }
762 
763  if(early)
764  {
765  entry.first->second.early=true;
766 
767  for(const auto &d : local_deps)
768  {
769  auto td_entry=typedef_map.find(d);
770  PRECONDITION(td_entry!=typedef_map.end());
771  td_entry->second.early=true;
772  }
773  }
774 
775  dependencies.insert(typedef_str);
776  }
777 
778  dependencies.insert(local_deps.begin(), local_deps.end());
779 }
780 
783 {
784  // sort the symbols first to ensure deterministic replacement in
785  // typedef_types below as there could be redundant declarations
786  // typedef int x;
787  // typedef int y;
788  std::map<std::string, symbolt> symbols_sorted;
789  for(const auto &symbol_entry : copied_symbol_table.symbols)
790  symbols_sorted.insert(
791  {id2string(symbol_entry.first), symbol_entry.second});
792 
793  for(const auto &symbol_entry : symbols_sorted)
794  {
795  const symbolt &symbol=symbol_entry.second;
796 
797  if(symbol.is_macro && symbol.is_type &&
798  symbol.location.get_function().empty())
799  {
800  const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
801  PRECONDITION(!typedef_str.empty());
802  typedef_types[symbol.type]=typedef_str;
804  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
805  else
806  collect_typedefs(symbol.type, false);
807  }
808  }
809 }
810 
813 void dump_ct::dump_typedefs(std::ostream &os) const
814 {
815  // we need to compute a topological sort; we do so by picking all
816  // typedefs the dependencies of which have been emitted into to_insert
817  std::vector<typedef_infot> typedefs_sorted;
818  typedefs_sorted.reserve(typedef_map.size());
819 
820  // elements in to_insert are lexicographically sorted and ready for
821  // output
822  std::map<std::string, typedef_infot> to_insert;
823 
824  std::unordered_set<irep_idt> typedefs_done;
825  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> forward_deps,
826  reverse_deps;
827 
828  for(const auto &td : typedef_map)
829  if(!td.second.type_decl_str.empty())
830  {
831  if(td.second.dependencies.empty())
832  // those can be dumped immediately
833  to_insert.insert({id2string(td.first), td.second});
834  else
835  {
836  // delay them until dependencies are dumped
837  forward_deps.insert({td.first, td.second.dependencies});
838  for(const auto &d : td.second.dependencies)
839  reverse_deps[d].insert(td.first);
840  }
841  }
842 
843  while(!to_insert.empty())
844  {
845  // the topologically next element (lexicographically ranked first
846  // among all the dependencies of which have been dumped)
847  typedef_infot t=to_insert.begin()->second;
848  to_insert.erase(to_insert.begin());
849  // move to the output queue
850  typedefs_sorted.push_back(t);
851 
852  // find any depending typedefs that are now valid, or at least
853  // reduce the remaining dependencies
854  auto r_it=reverse_deps.find(t.typedef_name);
855  if(r_it==reverse_deps.end())
856  continue;
857 
858  // reduce remaining dependencies
859  std::unordered_set<irep_idt> &r_deps = r_it->second;
860  for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
861  it != r_deps.end();) // no ++it
862  {
863  auto f_it=forward_deps.find(*it);
864  if(f_it==forward_deps.end()) // might be done already
865  {
866  it=r_deps.erase(it);
867  continue;
868  }
869 
870  // update dependencies
871  std::unordered_set<irep_idt> &f_deps = f_it->second;
872  PRECONDITION(!f_deps.empty());
873  PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
874  f_deps.erase(t.typedef_name);
875 
876  if(f_deps.empty()) // all depenencies done now!
877  {
878  const auto td_entry=typedef_map.find(*it);
879  PRECONDITION(td_entry!=typedef_map.end());
880  to_insert.insert({id2string(*it), td_entry->second});
881  forward_deps.erase(*it);
882  it=r_deps.erase(it);
883  }
884  else
885  ++it;
886  }
887  }
888 
889  POSTCONDITION(forward_deps.empty());
890 
891  for(const auto &td : typedefs_sorted)
892  os << td.type_decl_str << '\n';
893 
894  if(!typedefs_sorted.empty())
895  os << '\n';
896 }
897 
899  const symbolt &symbol,
900  std::ostream &os,
901  local_static_declst &local_static_decls)
902 {
903  const irep_idt &func=symbol.location.get_function();
904  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
905  !converted_global.insert(symbol.name).second)
906  return;
907 
908  code_declt d(symbol.symbol_expr());
909 
910  find_symbols_sett syms;
911  if(symbol.value.is_not_nil())
912  find_symbols_or_nexts(symbol.value, syms);
913 
914  // add a tentative declaration to cater for symbols in the initializer
915  // relying on it this symbol
916  if((func.empty() || symbol.is_extern) &&
917  (symbol.value.is_nil() || !syms.empty()))
918  {
919  os << "// " << symbol.name << '\n';
920  os << "// " << symbol.location << '\n';
921  os << expr_to_string(d) << '\n';
922  }
923 
924  if(!symbol.value.is_nil())
925  {
926  std::set<std::string> symbols_sorted;
927  for(find_symbols_sett::const_iterator
928  it=syms.begin();
929  it!=syms.end();
930  ++it)
931  {
932  bool inserted=symbols_sorted.insert(id2string(*it)).second;
933  CHECK_RETURN(inserted);
934  }
935 
936  for(std::set<std::string>::const_iterator
937  it=symbols_sorted.begin();
938  it!=symbols_sorted.end();
939  ++it)
940  {
941  const symbolt &sym=ns.lookup(*it);
942  if(!sym.is_type && sym.is_static_lifetime && sym.type.id()!=ID_code)
943  convert_global_variable(sym, os, local_static_decls);
944  }
945 
946  d.copy_to_operands(symbol.value);
947  }
948 
949  if(!func.empty() && !symbol.is_extern)
950  {
951  local_static_decls.emplace(symbol.name, d);
952  }
953  else if(!symbol.value.is_nil())
954  {
955  os << "// " << symbol.name << '\n';
956  os << "// " << symbol.location << '\n';
957 
958  std::list<irep_idt> empty_static, empty_types;
959  cleanup_decl(d, empty_static, empty_types);
960  CHECK_RETURN(empty_static.empty());
961  os << expr_to_string(d) << '\n';
962  }
963 }
964 
969 {
971  code_blockt decls;
972 
973  const symbolt *argc_sym=nullptr;
974  if(!ns.lookup("argc'", argc_sym))
975  {
976  symbol_exprt argc("argc", argc_sym->type);
977  replace.insert(argc_sym->symbol_expr(), argc);
978  code_declt d(argc);
979  decls.add(d);
980  }
981  const symbolt *argv_sym=nullptr;
982  if(!ns.lookup("argv'", argv_sym))
983  {
984  symbol_exprt argv("argv", argv_sym->type);
985  // replace argc' by argc in the type of argv['] to maintain type consistency
986  // while replacing
987  replace(argv);
988  replace.insert(symbol_exprt(argv_sym->name, argv.type()), argv);
989  code_declt d(argv);
990  decls.add(d);
991  }
992  const symbolt *return_sym=nullptr;
993  if(!ns.lookup("return'", return_sym))
994  {
995  symbol_exprt return_value("return_value", return_sym->type);
996  replace.insert(return_sym->symbol_expr(), return_value);
997  code_declt d(return_value);
998  decls.add(d);
999  }
1000 
1001  for(auto &code : b.statements())
1002  {
1003  if(code.get_statement()==ID_function_call)
1004  {
1005  exprt &func=to_code_function_call(code).function();
1006  if(func.id()==ID_symbol)
1007  {
1008  symbol_exprt &s=to_symbol_expr(func);
1009  if(s.get_identifier()==ID_main)
1011  else if(s.get_identifier() == INITIALIZE_FUNCTION)
1012  continue;
1013  }
1014  }
1015 
1016  decls.add(code);
1017  }
1018 
1019  b.swap(decls);
1020  replace(b);
1021 }
1022 
1024  const symbolt &symbol,
1025  const bool skip_main,
1026  std::ostream &os_decl,
1027  std::ostream &os_body,
1028  local_static_declst &local_static_decls)
1029 {
1030  // don't dump artificial main
1031  if(skip_main && symbol.name==goto_functionst::entry_point())
1032  return;
1033 
1034  // convert the goto program back to code - this might change
1035  // the function type
1036  goto_functionst::function_mapt::const_iterator func_entry=
1037  goto_functions.function_map.find(symbol.name);
1038  if(func_entry!=goto_functions.function_map.end() &&
1039  func_entry->second.body_available())
1040  {
1041  code_blockt b;
1042  std::list<irep_idt> type_decls, local_static;
1043 
1044  std::unordered_set<irep_idt> typedef_names;
1045  for(const auto &td : typedef_map)
1046  typedef_names.insert(td.first);
1047 
1048  goto_program2codet p2s(
1049  symbol.name,
1050  func_entry->second.body,
1052  b,
1053  local_static,
1054  type_decls,
1055  typedef_names,
1056  system_headers);
1057  p2s();
1058 
1060  b,
1061  local_static,
1062  local_static_decls,
1063  type_decls);
1064 
1065  convertedt converted_c_bak(converted_compound);
1066  convertedt converted_e_bak(converted_enum);
1067 
1069  enum_constants_bak(declared_enum_constants);
1070 
1072  b,
1073  type_decls);
1074 
1075  converted_enum.swap(converted_e_bak);
1076  converted_compound.swap(converted_c_bak);
1077 
1078  if(harness && symbol.name==goto_functions.entry_point())
1079  cleanup_harness(b);
1080 
1081  os_body << "// " << symbol.name << '\n';
1082  os_body << "// " << symbol.location << '\n';
1083  if(symbol.name==goto_functions.entry_point())
1084  os_body << make_decl(ID_main, symbol.type) << '\n';
1085  else if(!harness || symbol.name!=ID_main)
1086  os_body << make_decl(symbol.name, symbol.type) << '\n';
1087  else if(harness && symbol.name==ID_main)
1088  {
1089  os_body << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1090  << '\n';
1091  }
1092  os_body << expr_to_string(b);
1093  os_body << "\n\n";
1094 
1095  declared_enum_constants.swap(enum_constants_bak);
1096  }
1097 
1098  if(symbol.name!=goto_functionst::entry_point() &&
1099  symbol.name!=ID_main)
1100  {
1101  os_decl << "// " << symbol.name << '\n';
1102  os_decl << "// " << symbol.location << '\n';
1103  os_decl << make_decl(symbol.name, symbol.type) << ";\n";
1104  }
1105  else if(harness && symbol.name==ID_main)
1106  {
1107  os_decl << "// " << symbol.name << '\n';
1108  os_decl << "// " << symbol.location << '\n';
1109  os_decl << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1110  << ";\n";
1111  }
1112 
1113  // make sure typedef names used in the function declaration are
1114  // available
1115  collect_typedefs(symbol.type, true);
1116 }
1117 
1119  const irep_idt &identifier,
1120  codet &root,
1121  code_blockt* &dest,
1122  exprt::operandst::iterator &before)
1123 {
1124  if(!root.has_operands())
1125  return false;
1126 
1127  code_blockt *our_dest=nullptr;
1128 
1129  exprt::operandst &operands=root.operands();
1130  exprt::operandst::iterator first_found=operands.end();
1131 
1132  Forall_expr(it, operands)
1133  {
1134  bool found=false;
1135 
1136  // be aware of the skip-carries-type hack
1137  if(it->id()==ID_code &&
1138  to_code(*it).get_statement()!=ID_skip)
1140  identifier,
1141  to_code(*it),
1142  our_dest,
1143  before);
1144  else
1145  {
1146  find_symbols_sett syms;
1147  find_type_and_expr_symbols(*it, syms);
1148 
1149  found=syms.find(identifier)!=syms.end();
1150  }
1151 
1152  if(!found)
1153  continue;
1154 
1155  if(!our_dest)
1156  {
1157  // first containing block
1158  if(root.get_statement()==ID_block)
1159  {
1160  dest=&(to_code_block(root));
1161  before=it;
1162  }
1163 
1164  return true;
1165  }
1166  else
1167  {
1168  // there is a containing block and this is the first operand
1169  // that contains identifier
1170  if(first_found==operands.end())
1171  first_found=it;
1172  // we have seen it already - pick the first occurrence in this
1173  // block
1174  else if(root.get_statement()==ID_block)
1175  {
1176  dest=&(to_code_block(root));
1177  before=first_found;
1178 
1179  return true;
1180  }
1181  // we have seen it already - outer block has to deal with this
1182  else
1183  return true;
1184  }
1185  }
1186 
1187  if(first_found!=operands.end())
1188  {
1189  dest=our_dest;
1190 
1191  return true;
1192  }
1193 
1194  return false;
1195 }
1196 
1198  code_blockt &b,
1199  const std::list<irep_idt> &local_static,
1200  local_static_declst &local_static_decls,
1201  std::list<irep_idt> &type_decls)
1202 {
1203  // look up last identifier first as its value may introduce the
1204  // other ones
1205  for(std::list<irep_idt>::const_reverse_iterator
1206  it=local_static.rbegin();
1207  it!=local_static.rend();
1208  ++it)
1209  {
1210  local_static_declst::const_iterator d_it=
1211  local_static_decls.find(*it);
1212  PRECONDITION(d_it!=local_static_decls.end());
1213 
1214  code_declt d=d_it->second;
1215  std::list<irep_idt> redundant;
1216  cleanup_decl(d, redundant, type_decls);
1217 
1218  code_blockt *dest_ptr=nullptr;
1219  exprt::operandst::iterator before=b.operands().end();
1220 
1221  // some use of static variables might be optimised out if it is
1222  // within an if(false) { ... } block
1223  if(find_block_position_rec(*it, b, dest_ptr, before))
1224  {
1225  CHECK_RETURN(dest_ptr!=nullptr);
1226  dest_ptr->operands().insert(before, d);
1227  }
1228  }
1229 }
1230 
1232  code_blockt &b,
1233  const std::list<irep_idt> &type_decls)
1234 {
1235  // look up last identifier first as its value may introduce the
1236  // other ones
1237  for(std::list<irep_idt>::const_reverse_iterator
1238  it=type_decls.rbegin();
1239  it!=type_decls.rend();
1240  ++it)
1241  {
1242  const typet &type=ns.lookup(*it).type;
1243  // feed through plain C to expr2c by ending and re-starting
1244  // a comment block ...
1245  std::ostringstream os_body;
1246  os_body << *it << " */\n";
1247  irep_idt tag_kind =
1248  type.id() == ID_c_enum
1249  ? ID_c_enum_tag
1250  : (type.id() == ID_union ? ID_union_tag : ID_struct_tag);
1251  convert_compound(type, tag_typet(tag_kind, *it), false, os_body);
1252  os_body << "/*";
1253 
1254  code_skipt skip;
1255  skip.add_source_location().set_comment(os_body.str());
1256  // another hack to ensure symbols inside types are seen
1257  skip.type()=type;
1258 
1259  code_blockt *dest_ptr=nullptr;
1260  exprt::operandst::iterator before=b.operands().end();
1261 
1262  // we might not find it in case a transparent union type cast
1263  // has been removed by cleanup operations
1264  if(find_block_position_rec(*it, b, dest_ptr, before))
1265  {
1266  CHECK_RETURN(dest_ptr!=nullptr);
1267  dest_ptr->operands().insert(before, skip);
1268  }
1269  }
1270 }
1271 
1273 {
1274  Forall_operands(it, expr)
1275  cleanup_expr(*it);
1276 
1277  cleanup_type(expr.type());
1278 
1279  if(expr.id()==ID_struct)
1280  {
1281  struct_typet type=
1282  to_struct_type(ns.follow(expr.type()));
1283 
1284  struct_union_typet::componentst old_components;
1285  old_components.swap(type.components());
1286 
1287  exprt::operandst old_ops;
1288  old_ops.swap(expr.operands());
1289 
1290  PRECONDITION(old_components.size()==old_ops.size());
1291  exprt::operandst::iterator o_it=old_ops.begin();
1292  for(const auto &old_comp : old_components)
1293  {
1294  const bool is_zero_bit_field =
1295  old_comp.type().id() == ID_c_bit_field &&
1296  to_c_bit_field_type(old_comp.type()).get_width() == 0;
1297 
1298  if(!old_comp.get_is_padding() && !is_zero_bit_field)
1299  {
1300  type.components().push_back(old_comp);
1301  expr.add_to_operands(std::move(*o_it));
1302  }
1303  ++o_it;
1304  }
1305  expr.type().swap(type);
1306  }
1307  else if(expr.id()==ID_union)
1308  {
1309  union_exprt &u=to_union_expr(expr);
1310  const union_typet &u_type_f=to_union_type(ns.follow(u.type()));
1311 
1312  if(!u.type().get_bool(ID_C_transparent_union) &&
1313  !u_type_f.get_bool(ID_C_transparent_union))
1314  {
1315  if(u_type_f.get_component(u.get_component_name()).get_is_padding())
1316  // we just use an empty struct to fake an empty union
1317  expr = struct_exprt({}, struct_typet());
1318  }
1319  // add a typecast for NULL
1320  else if(u.op().id()==ID_constant &&
1321  u.op().type().id()==ID_pointer &&
1322  u.op().type().subtype().id()==ID_empty &&
1323  (u.op().is_zero() ||
1324  to_constant_expr(u.op()).get_value()==ID_NULL))
1325  {
1326  const struct_union_typet::componentt &comp=
1327  u_type_f.get_component(u.get_component_name());
1328  const typet &u_op_type=comp.type();
1329  PRECONDITION(u_op_type.id()==ID_pointer);
1330 
1331  typecast_exprt tc(u.op(), u_op_type);
1332  expr.swap(tc);
1333  }
1334  else
1335  {
1336  exprt tmp;
1337  tmp.swap(u.op());
1338  expr.swap(tmp);
1339  }
1340  }
1341  else if(
1342  expr.id() == ID_typecast &&
1343  to_typecast_expr(expr).op().id() == ID_typecast &&
1344  expr.type() == to_typecast_expr(expr).op().type())
1345  {
1346  exprt tmp = to_typecast_expr(expr).op();
1347  expr.swap(tmp);
1348  }
1349  else if(expr.id()==ID_code &&
1350  to_code(expr).get_statement()==ID_function_call &&
1351  to_code_function_call(to_code(expr)).function().id()==ID_symbol)
1352  {
1354  const symbol_exprt &fn=to_symbol_expr(call.function());
1355  code_function_callt::argumentst &arguments=call.arguments();
1356 
1357  // don't edit function calls we might have introduced
1358  const symbolt *s;
1359  if(!ns.lookup(fn.get_identifier(), s))
1360  {
1361  const symbolt &fn_sym=ns.lookup(fn.get_identifier());
1362  const code_typet &code_type=to_code_type(fn_sym.type);
1363  const code_typet::parameterst &parameters=code_type.parameters();
1364 
1365  if(parameters.size()==arguments.size())
1366  {
1367  code_typet::parameterst::const_iterator it=parameters.begin();
1368  for(auto &argument : arguments)
1369  {
1370  const typet &type=ns.follow(it->type());
1371  if(type.id()==ID_union &&
1372  type.get_bool(ID_C_transparent_union))
1373  {
1374  if(argument.id() == ID_typecast && argument.type() == type)
1375  argument = to_typecast_expr(argument).op();
1376 
1377  // add a typecast for NULL or 0
1378  if(
1379  argument.id() == ID_constant &&
1380  (argument.is_zero() ||
1381  to_constant_expr(argument).get_value() == ID_NULL))
1382  {
1383  const typet &comp_type=
1384  to_union_type(type).components().front().type();
1385 
1386  if(comp_type.id()==ID_pointer)
1387  argument = typecast_exprt(argument, comp_type);
1388  }
1389  }
1390 
1391  ++it;
1392  }
1393  }
1394  }
1395  }
1396  else if(expr.id()==ID_constant &&
1397  expr.type().id()==ID_signedbv)
1398  {
1399  #if 0
1400  const irep_idt &cformat=expr.get(ID_C_cformat);
1401 
1402  if(!cformat.empty())
1403  {
1404  declared_enum_constants_mapt::const_iterator entry=
1405  declared_enum_constants.find(cformat);
1406 
1407  if(entry!=declared_enum_constants.end() &&
1408  entry->first!=entry->second)
1409  expr.set(ID_C_cformat, entry->second);
1410  else if(entry==declared_enum_constants.end() &&
1411  !std::isdigit(id2string(cformat)[0]))
1412  expr.remove(ID_C_cformat);
1413  }
1414  #endif
1415  }
1416  else if(
1417  expr.id() == ID_byte_update_little_endian ||
1418  expr.id() == ID_byte_update_big_endian)
1419  {
1420  const byte_update_exprt &bu = to_byte_update_expr(expr);
1421 
1422  if(bu.op().id() == ID_union && bu.offset().is_zero())
1423  {
1424  const union_exprt &union_expr = to_union_expr(bu.op());
1425  const union_typet &union_type =
1426  to_union_type(ns.follow(union_expr.type()));
1427 
1428  for(const auto &comp : union_type.components())
1429  {
1430  if(bu.value().type() == comp.type())
1431  {
1432  exprt member1{ID_member};
1433  member1.set(ID_component_name, union_expr.get_component_name());
1434  exprt designated_initializer1{ID_designated_initializer};
1435  designated_initializer1.add_to_operands(union_expr.op());
1436  designated_initializer1.add(ID_designator).move_to_sub(member1);
1437 
1438  exprt member2{ID_member};
1439  member2.set(ID_component_name, comp.get_name());
1440  exprt designated_initializer2{ID_designated_initializer};
1441  designated_initializer2.add_to_operands(bu.value());
1442  designated_initializer2.add(ID_designator).move_to_sub(member2);
1443 
1444  binary_exprt initializer_list{std::move(designated_initializer1),
1445  ID_initializer_list,
1446  std::move(designated_initializer2)};
1447  expr.swap(initializer_list);
1448 
1449  return;
1450  }
1451  }
1452  }
1453  else if(
1454  bu.op().id() == ID_side_effect &&
1455  to_side_effect_expr(bu.op()).get_statement() == ID_nondet &&
1456  ns.follow(bu.op().type()).id() == ID_union && bu.offset().is_zero())
1457  {
1458  const union_typet &union_type = to_union_type(ns.follow(bu.op().type()));
1459 
1460  for(const auto &comp : union_type.components())
1461  {
1462  if(bu.value().type() == comp.type())
1463  {
1464  union_exprt union_expr{comp.get_name(), bu.value(), bu.op().type()};
1465  expr.swap(union_expr);
1466 
1467  return;
1468  }
1469  }
1470  }
1471 
1472  optionalt<exprt> clean_init;
1473  if(
1474  ns.follow(bu.type()).id() == ID_union &&
1476  {
1477  clean_init = zero_initializer(bu.op().type(), source_locationt{}, ns)
1478  .value_or(nil_exprt{});
1479  if(clean_init->id() != ID_struct || clean_init->has_operands())
1480  cleanup_expr(*clean_init);
1481  }
1482 
1483  if(clean_init.has_value() && bu.op() == *clean_init)
1484  {
1485  const union_typet &union_type = to_union_type(ns.follow(bu.type()));
1486 
1487  for(const auto &comp : union_type.components())
1488  {
1489  if(bu.value().type() == comp.type())
1490  {
1491  union_exprt union_expr{comp.get_name(), bu.value(), bu.type()};
1492  expr.swap(union_expr);
1493 
1494  return;
1495  }
1496  }
1497 
1498  // we still haven't found a suitable component, so just ignore types and
1499  // build an initializer list without designators
1500  expr = unary_exprt{ID_initializer_list, bu.value()};
1501  }
1502  }
1503 }
1504 
1506 {
1507  for(typet &subtype : to_type_with_subtypes(type).subtypes())
1508  cleanup_type(subtype);
1509 
1510  if(type.id()==ID_code)
1511  {
1512  code_typet &code_type=to_code_type(type);
1513 
1514  cleanup_type(code_type.return_type());
1515 
1516  for(code_typet::parameterst::iterator
1517  it=code_type.parameters().begin();
1518  it!=code_type.parameters().end();
1519  ++it)
1520  cleanup_type(it->type());
1521  }
1522 
1523  if(type.id()==ID_array)
1524  cleanup_expr(to_array_type(type).size());
1525 
1526  POSTCONDITION(
1527  (type.id()!=ID_union && type.id()!=ID_struct) ||
1528  !type.get(ID_tag).empty());
1529 }
1530 
1532 {
1533  // future TODO: with C++20 we can actually use designated initializers as
1534  // commented out below
1535  static expr2c_configurationt configuration{
1536  /* .include_struct_padding_components = */ true,
1537  /* .print_struct_body_in_type = */ true,
1538  /* .include_array_size = */ true,
1539  /* .true_string = */ "1",
1540  /* .false_string = */ "0",
1541  /* .use_library_macros = */ true,
1542  /* .print_enum_int_value = */ false,
1543  /* .expand_typedef = */ false};
1544 
1545  return configuration;
1546 }
1547 
1548 std::string dump_ct::type_to_string(const typet &type)
1549 {
1550  std::string ret;
1551  typet t=type;
1552  cleanup_type(t);
1553 
1554  if(mode == ID_C)
1555  return type2c(t, ns, expr2c_configuration());
1556  else if(mode == ID_cpp)
1557  return type2cpp(t, ns);
1558  else
1559  UNREACHABLE;
1560 }
1561 
1562 std::string dump_ct::expr_to_string(const exprt &expr)
1563 {
1564  std::string ret;
1565  exprt e=expr;
1566  cleanup_expr(e);
1567 
1568  if(mode == ID_C)
1569  return expr2c(e, ns, expr2c_configuration());
1570  else if(mode == ID_cpp)
1571  return expr2cpp(e, ns);
1572  else
1573  UNREACHABLE;
1574 }
1575 
1576 void dump_c(
1577  const goto_functionst &src,
1578  const bool use_system_headers,
1579  const bool use_all_headers,
1580  const bool include_harness,
1581  const namespacet &ns,
1582  std::ostream &out)
1583 {
1584  dump_ct goto2c(
1585  src, use_system_headers, use_all_headers, include_harness, ns, ID_C);
1586  out << goto2c;
1587 }
1588 
1590  const goto_functionst &src,
1591  const bool use_system_headers,
1592  const bool use_all_headers,
1593  const bool include_harness,
1594  const namespacet &ns,
1595  std::ostream &out)
1596 {
1597  dump_ct goto2cpp(
1598  src, use_system_headers, use_all_headers, include_harness, ns, ID_cpp);
1599  out << goto2cpp;
1600 }
1601 
1602 static bool
1603 module_local_declaration(const symbolt &symbol, const std::string module)
1604 {
1605  std::string base_name =
1606  get_base_name(id2string(symbol.location.get_file()), true);
1607  std::string symbol_module = strip_string(id2string(symbol.module));
1608  return (base_name == module && symbol_module == module);
1609 }
1610 
1612  const goto_functionst &src,
1613  const bool use_system_headers,
1614  const bool use_all_headers,
1615  const bool include_harness,
1616  const namespacet &ns,
1617  const std::string module,
1618  std::ostream &out)
1619 {
1620  symbol_tablet symbol_table = ns.get_symbol_table();
1621  for(symbol_tablet::iteratort it = symbol_table.begin();
1622  it != symbol_table.end();
1623  it++)
1624  {
1625  symbolt &new_symbol = it.get_writeable_symbol();
1626  if(module_local_declaration(new_symbol, module))
1627  {
1628  new_symbol.type.set(ID_C_do_not_dump, 0);
1629  }
1630  else
1631  {
1632  new_symbol.type.set(ID_C_do_not_dump, 1);
1633  }
1634  }
1635 
1636  namespacet new_ns(symbol_table);
1637  dump_ct goto2c(
1638  src,
1639  use_system_headers,
1640  use_all_headers,
1641  include_harness,
1642  new_ns,
1643  ID_C,
1645  out << goto2c;
1646 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:133
dump_ct::declared_enum_constants_mapt
std::unordered_map< irep_idt, irep_idt > declared_enum_constants_mapt
Definition: dump_c_class.h:165
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:563
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
get_base_name
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Definition: get_base_name.cpp:16
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
dump_ct::collect_typedefs_rec
void collect_typedefs_rec(const typet &type, bool early, std::unordered_set< irep_idt > &dependencies)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
Definition: dump_c.cpp:705
Forall_expr
#define Forall_expr(it, expr)
Definition: expr.h:34
dump_c_configurationt::enable_include_headers
dump_c_configurationt enable_include_headers()
Definition: dump_c_class.h:99
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
tag_typet::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:454
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:628
dump_c_configurationt::disable_include_global_vars
dump_c_configurationt disable_include_global_vars()
Definition: dump_c_class.h:81
dump_ct::indent
static std::string indent(const unsigned n)
Definition: dump_c_class.h:189
dump_ct::goto_functions
const goto_functionst & goto_functions
Definition: dump_c_class.h:151
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
dump_c_configurationt::default_configuration
static dump_c_configurationt default_configuration
The default used for dump-c and dump-cpp.
Definition: dump_c_class.h:52
find_type_and_expr_symbols
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:200
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
dump_ct::ns
const namespacet ns
Definition: dump_c_class.h:153
codet::op0
exprt & op0()
Definition: expr.h:103
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:67
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:689
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
find_symbols_or_nexts
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
Definition: find_symbols.cpp:18
dump_c_configurationt
Used for configuring the behaviour of dump_c.
Definition: dump_c_class.h:22
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
find_non_pointer_type_symbols
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:186
byte_update_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:109
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: std_types.h:652
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
replace_symbol.h
code_declt::initial_value
optionalt< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
Definition: std_code.h:427
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:540
configt::main
optionalt< std::string > main
Definition: config.h:261
invariant.h
dump_c_configurationt::follow_compounds
bool follow_compounds
Define whether to follow compunds recursively.
Definition: dump_c_class.h:42
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
union_exprt
Union constructor from single element.
Definition: std_expr.h:1517
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:928
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
dump_ct::convert_function_declaration
void convert_function_declaration(const symbolt &symbol, const bool skip_main, std::ostream &os_decl, std::ostream &os_body, local_static_declst &local_static_decls)
Definition: dump_c.cpp:1023
dump_ct::system_symbols
system_library_symbolst system_symbols
Definition: dump_c_class.h:163
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:282
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1563
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:498
expr2cpp.h
dump_ct::convert_compound
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
Definition: dump_c.cpp:373
irep_idt
dstringt irep_idt
Definition: irep.h:37
code_declt::set_initial_value
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
Definition: std_code.h:438
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
find_block_position_rec
static bool find_block_position_rec(const irep_idt &identifier, codet &root, code_blockt *&dest, exprt::operandst::iterator &before)
Definition: dump_c.cpp:1118
expr2cpp
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:490
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
configt::ansi_c
struct configt::ansi_ct ansi_c
dump_c_configurationt::disable_include_function_bodies
dump_c_configurationt disable_include_function_bodies()
Definition: dump_c_class.h:63
expr2c_configuration
static expr2c_configurationt expr2c_configuration()
Definition: dump_c.cpp:1531
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
dump_ct::typedef_map
typedef_mapt typedef_map
Definition: dump_c_class.h:182
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
dump_ct::insert_local_type_decls
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1231
dump_ct::expr_to_string
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1562
dump_ct::converted_compound
convertedt converted_compound
Definition: dump_c_class.h:159
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
symbol_tablet::begin
virtual iteratort begin() override
Definition: symbol_table.h:114
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:538
dump_ct::harness
const bool harness
Definition: dump_c_class.h:156
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
dump_ct::system_headers
std::set< std::string > system_headers
Definition: dump_c_class.h:161
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
dump_ct::make_decl
std::string make_decl(const irep_idt &identifier, const typet &type)
Definition: dump_c_class.h:194
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1583
dump_ct::dump_typedefs
void dump_typedefs(std::ostream &os) const
Print all typedefs that are not covered via typedef struct xyz { ...
Definition: dump_c.cpp:813
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
dump_ct::declared_enum_constants
declared_enum_constants_mapt declared_enum_constants
Definition: dump_c_class.h:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
dump_c_configurationt::include_typedefs
bool include_typedefs
Include the typedefs in the dump.
Definition: dump_c_class.h:33
operator<<
std::ostream & operator<<(std::ostream &out, dump_ct &src)
Definition: dump_c.cpp:41
strip_string
std::string strip_string(const std::string &s)
Remove all whitespace characters from either end of a string.
Definition: string_utils.cpp:21
dump_ct::converted_global
convertedt converted_global
Definition: dump_c_class.h:159
byte_operators.h
Expression classes for byte-level operators.
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
expr_initializer.h
Expression Initialization.
find_symbols.h
dump_ct::cleanup_type
void cleanup_type(typet &type)
Definition: dump_c.cpp:1505
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:483
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1255
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
symbol_tablet::end
virtual iteratort end() override
Definition: symbol_table.h:118
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
system_library_symbolst::is_type_internal
bool is_type_internal(const typet &type, std::set< std::string > &out_system_headers) const
Helper function to call is_symbol_internal_symbol on a nameless fake symbol with the given type,...
Definition: system_library_symbols.cpp:263
dump_ct::convert_compound_enum
void convert_compound_enum(const typet &type, std::ostream &os)
Definition: dump_c.cpp:605
dump_ct::cleanup_expr
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1272
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:120
type2cpp
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:497
dump_ct::local_static_declst
std::unordered_map< irep_idt, code_declt > local_static_declst
Definition: dump_c_class.h:233
expr2c.h
dump_c
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1576
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3921
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
struct_union_typet::componentt::get_is_padding
bool get_is_padding() const
Definition: std_types.h:124
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1272
dump_ct::convertedt
std::unordered_set< irep_idt > convertedt
Definition: dump_c_class.h:158
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1478
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
module_local_declaration
static bool module_local_declaration(const symbolt &symbol, const std::string module)
Definition: dump_c.cpp:1603
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
dump_c_type_header
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
Definition: dump_c.cpp:1611
dump_ct::cleanup_decl
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Definition: dump_c.cpp:648
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:116
goto_program2code.h
Dump Goto-Program as C/C++ Source.
irept::swap
void swap(irept &irep)
Definition: irep.h:452
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
dump_ct::insert_local_static_decls
void insert_local_static_decls(code_blockt &b, const std::list< irep_idt > &local_static, local_static_declst &local_static_decls, std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1197
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
dstringt::empty
bool empty() const
Definition: dstring.h:88
get_base_name.h
dump_c_configurationt::include_compounds
bool include_compounds
Include struct definitions in the dump.
Definition: dump_c_class.h:39
dump_ct::operator()
void operator()(std::ostream &out)
Definition: dump_c.cpp:47
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
union_typet
The union type.
Definition: std_types.h:393
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:445
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
dump_c_configurationt::include_headers
bool include_headers
Include headers type declarations are borrowed from.
Definition: dump_c_class.h:45
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
dump_c_configurationt::include_function_decls
bool include_function_decls
Include the function declarations in the dump.
Definition: dump_c_class.h:24
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1920
config
configt config
Definition: config.cpp:24
source_locationt
Definition: source_location.h:20
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1048
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1525
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
struct_union_typet::componentt
Definition: std_types.h:64
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
dump_ct::mode
const irep_idt mode
Definition: dump_c_class.h:155
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
dump_c_configurationt::include_global_decls
bool include_global_decls
Include the global declarations in the dump.
Definition: dump_c_class.h:30
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
byte_update_exprt::value
const exprt & value() const
Definition: byte_operators.h:110
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:704
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
dump_c_configurationt::disable_include_function_decls
dump_c_configurationt disable_include_function_decls()
Definition: dump_c_class.h:57
dump_c_configurationt::include_global_vars
bool include_global_vars
Include global variable definitions in the dump.
Definition: dump_c_class.h:36
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbol_table_baset::iteratort
Definition: symbol_table_base.h:155
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
dump_c_configurationt::include_function_bodies
bool include_function_bodies
Include the functions in the dump.
Definition: dump_c_class.h:27
dump_ct::typedef_infot::typedef_name
irep_idt typedef_name
Definition: dump_c_class.h:170
dump_c_class.h
Dump Goto-Program as C/C++ Source.
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
dump_ct::copied_symbol_table
symbol_tablet copied_symbol_table
Definition: dump_c_class.h:152
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
dump_ct::typedef_infot
Definition: dump_c_class.h:169
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
dump_ct::typedef_types
typedef_typest typedef_types
Definition: dump_c_class.h:184
symbolt::is_type
bool is_type
Definition: symbol.h:61
dump_ct::cleanup_harness
void cleanup_harness(code_blockt &b)
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
Definition: dump_c.cpp:968
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1305
goto_program2codet
Definition: goto_program2code.h:21
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
irept::get_sub
subt & get_sub()
Definition: irep.h:466
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:140
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
config.h
dump_ct::convert_compound_declaration
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Definition: dump_c.cpp:341
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
system_library_symbolst::is_symbol_internal_symbol
bool is_symbol_internal_symbol(const symbolt &symbol, std::set< std::string > &out_system_headers) const
To find out if a symbol is an internal symbol.
Definition: system_library_symbols.cpp:277
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
dump_ct::dump_c_config
const dump_c_configurationt dump_c_config
Definition: dump_c_class.h:154
dump_c_configurationt::type_header_configuration
static dump_c_configurationt type_header_configuration
The config used for dump-c-type-header.
Definition: dump_c_class.h:55
dump_ct::convert_global_variable
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
Definition: dump_c.cpp:898
exprt::operands
operandst & operands()
Definition: expr.h:96
type2c
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3937
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430
dump_ct::collect_typedefs
void collect_typedefs(const typet &type, bool early)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
Definition: dump_c.cpp:692
static_lifetime_init.h
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
expr2c_configurationt
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:21
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
dump_c.h
Dump C from Goto Program.
dump_ct
Definition: dump_c_class.h:107
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
byte_update_exprt::op
const exprt & op() const
Definition: byte_operators.h:108
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:105
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
dump_cpp
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1589
dump_ct::type_to_string
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1548
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
dump_ct::converted_enum
convertedt converted_enum
Definition: dump_c_class.h:159
dump_ct::gather_global_typedefs
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.
Definition: dump_c.cpp:782
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701