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/base_type.h>
15 #include <util/config.h>
16 #include <util/find_symbols.h>
17 #include <util/invariant.h>
18 #include <util/replace_symbol.h>
19 
20 #include <ansi-c/ansi_c_language.h>
21 #include <cpp/cpp_language.h>
22 
24 
25 #include "dump_c_class.h"
26 #include "goto_program2code.h"
27 
28 inline std::ostream &operator << (std::ostream &out, dump_ct &src)
29 {
30  src(out);
31  return out;
32 }
33 
34 void dump_ct::operator()(std::ostream &os)
35 {
36  std::stringstream func_decl_stream;
37  std::stringstream compound_body_stream;
38  std::stringstream global_var_stream;
39  std::stringstream global_decl_stream;
40  std::stringstream func_body_stream;
41  local_static_declst local_static_decls;
42 
43  // add copies of struct types when ID_C_transparent_union is only
44  // annotated to parameter
45  symbol_tablet symbols_transparent;
46  for(const auto &named_symbol : copied_symbol_table.symbols)
47  {
48  const symbolt &symbol=named_symbol.second;
49 
50  if(symbol.type.id()!=ID_code)
51  continue;
52 
53  code_typet &code_type=to_code_type(
54  copied_symbol_table.get_writeable_ref(named_symbol.first).type);
55  code_typet::parameterst &parameters=code_type.parameters();
56 
57  for(code_typet::parameterst::iterator
58  it2=parameters.begin();
59  it2!=parameters.end();
60  ++it2)
61  {
62  typet &type=it2->type();
63 
64  if(type.id() == ID_symbol_type && type.get_bool(ID_C_transparent_union))
65  {
66  symbolt new_type_sym=
67  ns.lookup(to_symbol_type(type).get_identifier());
68 
69  new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
70  new_type_sym.type.set(ID_C_transparent_union, true);
71 
72  // we might have it already, in which case this has no effect
73  symbols_transparent.add(new_type_sym);
74 
75  to_symbol_type(type).set_identifier(new_type_sym.name);
76  type.remove(ID_C_transparent_union);
77  }
78  }
79  }
80  for(const auto &symbol_pair : symbols_transparent.symbols)
81  {
82  copied_symbol_table.add(symbol_pair.second);
83  }
84 
85  typedef std::unordered_map<irep_idt, unsigned> unique_tagst;
86  unique_tagst unique_tags;
87 
88  // add tags to anonymous union/struct/enum,
89  // and prepare lexicographic order
90  std::set<std::string> symbols_sorted;
91  for(const auto &named_symbol : copied_symbol_table.symbols)
92  {
93  symbolt &symbol=*copied_symbol_table.get_writeable(named_symbol.first);
94  bool tag_added=false;
95 
96  // TODO we could get rid of some of the ID_anonymous by looking up
97  // the origin symbol types in typedef_types and adjusting any other
98  // uses of ID_tag
99  if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
100  symbol.type.get(ID_tag).empty())
101  {
102  PRECONDITION(symbol.is_type);
103  symbol.type.set(ID_tag, ID_anonymous);
104  tag_added=true;
105  }
106  else if(symbol.type.id()==ID_c_enum &&
107  symbol.type.find(ID_tag).get(ID_C_base_name).empty())
108  {
109  PRECONDITION(symbol.is_type);
110  symbol.type.add(ID_tag).set(ID_C_base_name, ID_anonymous);
111  tag_added=true;
112  }
113 
114  const std::string name_str=id2string(named_symbol.first);
115  if(symbol.is_type &&
116  (symbol.type.id()==ID_union ||
117  symbol.type.id()==ID_struct ||
118  symbol.type.id()==ID_c_enum))
119  {
120  std::string new_tag=symbol.type.id()==ID_c_enum?
121  symbol.type.find(ID_tag).get_string(ID_C_base_name):
122  symbol.type.get_string(ID_tag);
123 
124  std::string::size_type tag_pos=new_tag.rfind("tag-");
125  if(tag_pos!=std::string::npos)
126  new_tag.erase(0, tag_pos+4);
127  const std::string new_tag_base=new_tag;
128 
129  for(std::pair<unique_tagst::iterator, bool>
130  unique_entry=unique_tags.insert(std::make_pair(new_tag, 0));
131  !unique_entry.second;
132  unique_entry=unique_tags.insert(std::make_pair(new_tag, 0)))
133  {
134  new_tag=new_tag_base+"$"+
135  std::to_string(unique_entry.first->second);
136  ++(unique_entry.first->second);
137  }
138 
139  if(symbol.type.id()==ID_c_enum)
140  {
141  symbol.type.add(ID_tag).set(ID_C_base_name, new_tag);
142  symbol.base_name=new_tag;
143  }
144  else
145  symbol.type.set(ID_tag, new_tag);
146  }
147 
148  // we don't want to dump in full all definitions; in particular
149  // do not dump anonymous types that are defined in system headers
150  if((!tag_added || symbol.is_type) &&
152  symbol.name!=goto_functions.entry_point())
153  continue;
154 
155  bool inserted=symbols_sorted.insert(name_str).second;
156  CHECK_RETURN(inserted);
157  }
158 
160 
161  // collect all declarations we might need, include local static variables
162  bool skip_function_main=false;
163  for(std::set<std::string>::const_iterator
164  it=symbols_sorted.begin();
165  it!=symbols_sorted.end();
166  ++it)
167  {
168  const symbolt &symbol=ns.lookup(*it);
169  const irep_idt &type_id=symbol.type.id();
170 
171  if(symbol.is_type &&
172  symbol.location.get_function().empty() &&
173  (type_id==ID_struct ||
174  type_id==ID_incomplete_struct ||
175  type_id==ID_union ||
176  type_id==ID_incomplete_union ||
177  type_id==ID_c_enum))
178  {
180  {
181  global_decl_stream << "// " << symbol.name << '\n';
182  global_decl_stream << "// " << symbol.location << '\n';
183 
184  if(type_id==ID_c_enum)
185  convert_compound_enum(symbol.type, global_decl_stream);
186  else
187  global_decl_stream << type_to_string(symbol_typet(symbol.name))
188  << ";\n\n";
189  }
190  }
191  else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
193  symbol,
194  global_var_stream,
195  local_static_decls);
196  else if(symbol.type.id()==ID_code)
197  {
198  goto_functionst::function_mapt::const_iterator func_entry=
199  goto_functions.function_map.find(symbol.name);
200 
201  if(!harness &&
202  func_entry!=goto_functions.function_map.end() &&
203  func_entry->second.body_available() &&
204  (symbol.name==ID_main ||
205  (!config.main.empty() && symbol.name==config.main)))
206  skip_function_main=true;
207  }
208  }
209 
210  // function declarations and definitions
211  for(std::set<std::string>::const_iterator
212  it=symbols_sorted.begin();
213  it!=symbols_sorted.end();
214  ++it)
215  {
216  const symbolt &symbol=ns.lookup(*it);
217 
218  if(symbol.type.id()!=ID_code ||
219  symbol.is_type)
220  continue;
221 
223  symbol,
224  skip_function_main,
225  func_decl_stream,
226  func_body_stream,
227  local_static_decls);
228  }
229 
230  // (possibly modified) compound types
231  for(std::set<std::string>::const_iterator
232  it=symbols_sorted.begin();
233  it!=symbols_sorted.end();
234  ++it)
235  {
236  const symbolt &symbol=ns.lookup(*it);
237 
238  if(symbol.is_type &&
239  (symbol.type.id()==ID_struct ||
240  symbol.type.id()==ID_incomplete_struct ||
241  symbol.type.id()==ID_union ||
242  symbol.type.id()==ID_incomplete_union))
244  symbol,
245  compound_body_stream);
246  }
247 
248  // Dump the code to the target stream;
249  // the statements before to this point collect the code to dump!
250  for(std::set<std::string>::const_iterator
251  it=system_headers.begin();
252  it!=system_headers.end();
253  ++it)
254  os << "#include <" << *it << ">\n";
255  if(!system_headers.empty())
256  os << '\n';
257 
258  if(global_var_stream.str().find("NULL")!=std::string::npos ||
259  func_body_stream.str().find("NULL")!=std::string::npos)
260  {
261  os << "#ifndef NULL\n"
262  << "#define NULL ((void*)0)\n"
263  << "#endif\n\n";
264  }
265  if(func_body_stream.str().find("FENCE")!=std::string::npos)
266  {
267  os << "#ifndef FENCE\n"
268  << "#define FENCE(x) ((void)0)\n"
269  << "#endif\n\n";
270  }
271  if(func_body_stream.str().find("IEEE_FLOAT_")!=std::string::npos)
272  {
273  os << "#ifndef IEEE_FLOAT_EQUAL\n"
274  << "#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n"
275  << "#endif\n"
276  << "#ifndef IEEE_FLOAT_NOTEQUAL\n"
277  << "#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n"
278  << "#endif\n\n";
279  }
280 
281  if(!global_decl_stream.str().empty())
282  os << global_decl_stream.str() << '\n';
283 
284  dump_typedefs(os);
285 
286  if(!func_decl_stream.str().empty())
287  os << func_decl_stream.str() << '\n';
288  if(!compound_body_stream.str().empty())
289  os << compound_body_stream.str() << '\n';
290  if(!global_var_stream.str().empty())
291  os << global_var_stream.str() << '\n';
292  os << func_body_stream.str();
293 }
294 
297  const symbolt &symbol,
298  std::ostream &os_body)
299 {
300  if(!symbol.location.get_function().empty())
301  return;
302 
303  // do compound type body
304  if(symbol.type.id()==ID_struct ||
305  symbol.type.id()==ID_union ||
306  symbol.type.id()==ID_c_enum)
307  convert_compound(symbol.type, symbol_typet(symbol.name), true, os_body);
308 }
309 
311  const typet &type,
312  const typet &unresolved,
313  bool recursive,
314  std::ostream &os)
315 {
316  if(type.id() == ID_symbol_type)
317  {
318  const symbolt &symbol=
319  ns.lookup(to_symbol_type(type).get_identifier());
320  DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
321 
323  convert_compound(symbol.type, unresolved, recursive, os);
324  }
325  else if(
326  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
327  type.id() == ID_union_tag)
328  {
329  const symbolt &symbol = ns.lookup(to_tag_type(type));
330  DATA_INVARIANT(symbol.is_type, "tag expected to be type symbol");
331 
333  convert_compound(symbol.type, unresolved, recursive, os);
334  }
335  else if(type.id()==ID_array || type.id()==ID_pointer)
336  {
337  if(!recursive)
338  return;
339 
340  convert_compound(type.subtype(), type.subtype(), recursive, os);
341 
342  // sizeof may contain a type symbol that has to be declared first
343  if(type.id()==ID_array)
344  {
345  find_symbols_sett syms;
346  find_non_pointer_type_symbols(to_array_type(type).size(), syms);
347 
348  for(find_symbols_sett::const_iterator
349  it=syms.begin();
350  it!=syms.end();
351  ++it)
352  {
353  symbol_typet s_type(*it);
354  convert_compound(s_type, s_type, recursive, os);
355  }
356  }
357  }
358  else if(type.id()==ID_struct || type.id()==ID_union)
359  convert_compound(to_struct_union_type(type), unresolved, recursive, os);
360  else if(type.id()==ID_c_enum)
361  convert_compound_enum(type, os);
362 }
363 
365  const struct_union_typet &type,
366  const typet &unresolved,
367  bool recursive,
368  std::ostream &os)
369 {
370  const irep_idt &name=type.get(ID_tag);
371 
372  if(!converted_compound.insert(name).second)
373  return;
374 
375  // make sure typedef names used in the declaration are available
376  collect_typedefs(type, true);
377 
378  const irept &bases = type.find(ID_bases);
379  std::stringstream base_decls;
380  forall_irep(parent_it, bases.get_sub())
381  {
382  UNREACHABLE;
383  /*
384  assert(parent_it->id() == ID_base);
385  assert(parent_it->get(ID_type) == ID_symbol_type);
386 
387  const irep_idt &base_id=
388  parent_it->find(ID_type).get(ID_identifier);
389  const irep_idt &renamed_base_id=global_renaming[base_id];
390  const symbolt &parsymb=ns.lookup(renamed_base_id);
391 
392  convert_compound_rec(parsymb.type, os);
393 
394  base_decls << id2string(renamed_base_id) +
395  (parent_it+1==bases.get_sub().end()?"":", ");
396  */
397  }
398 
399  /*
400  // for the constructor
401  string constructor_args;
402  string constructor_body;
403 
404  std::string component_name = id2string(renaming[compo.get(ID_name)]);
405  assert(component_name != "");
406 
407  if(it != struct_type.components().begin()) constructor_args += ", ";
408 
409  if(compo.type().id() == ID_pointer)
410  constructor_args += type_to_string(compo.type()) + component_name;
411  else
412  constructor_args += "const " + type_to_string(compo.type()) + "& " + component_name;
413 
414  constructor_body += indent + indent + "this->"+component_name + " = " + component_name + ";\n";
415  */
416 
417  std::stringstream struct_body;
418 
419  for(const auto &comp : type.components())
420  {
421  const typet &comp_type=ns.follow(comp.type());
422 
423  if(comp_type.id()==ID_code ||
424  comp.get_bool(ID_from_base) ||
425  comp.get_is_padding())
426  continue;
427 
428  const typet *non_array_type=&ns.follow(comp_type);
429  while(non_array_type->id()==ID_array)
430  non_array_type=&(ns.follow(non_array_type->subtype()));
431 
432  if(recursive)
433  {
434  if(non_array_type->id()!=ID_pointer)
435  convert_compound(comp.type(), comp.type(), recursive, os);
436  else
437  collect_typedefs(comp.type(), true);
438  }
439 
440  irep_idt comp_name=comp.get_name();
441 
442  struct_body << indent(1) << "// " << comp_name << '\n';
443  struct_body << indent(1);
444 
445  // component names such as "main" would collide with other objects in the
446  // namespace
447  std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
448  std::string s=make_decl(fake_unique_name, comp.type());
449  POSTCONDITION(s.find("NO/SUCH/NS")==std::string::npos);
450 
451  if(comp_type.id()==ID_c_bit_field &&
452  to_c_bit_field_type(comp_type).get_width()==0)
453  {
454  comp_name="";
455  s=type_to_string(comp_type);
456  }
457 
458  if(s.find(CPROVER_PREFIX "bitvector") == std::string::npos)
459  {
460  struct_body << s;
461  }
462  else if(comp_type.id()==ID_signedbv)
463  {
464  const signedbv_typet &t=to_signedbv_type(comp_type);
466  struct_body << "long long int " << comp_name
467  << " : " << t.get_width();
468  else if(language->id()=="cpp")
469  struct_body << "__signedbv<" << t.get_width() << "> "
470  << comp_name;
471  else
472  struct_body << s;
473  }
474  else if(comp_type.id()==ID_unsignedbv)
475  {
476  const unsignedbv_typet &t=to_unsignedbv_type(comp_type);
478  struct_body << "unsigned long long " << comp_name
479  << " : " << t.get_width();
480  else if(language->id()=="cpp")
481  struct_body << "__unsignedbv<" << t.get_width() << "> "
482  << comp_name;
483  else
484  struct_body << s;
485  }
486  else
487  UNREACHABLE;
488 
489  struct_body << ";\n";
490  }
491 
492  typet unresolved_clean=unresolved;
493  typedef_typest::const_iterator td_entry=
494  typedef_types.find(unresolved);
495  irep_idt typedef_str;
496  if(td_entry!=typedef_types.end())
497  {
498  unresolved_clean.remove(ID_C_typedef);
499  typedef_str=td_entry->second;
500  std::pair<typedef_mapt::iterator, bool> td_map_entry=
501  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
502  PRECONDITION(!td_map_entry.second);
503  if(!td_map_entry.first->second.early)
504  td_map_entry.first->second.type_decl_str="";
505  os << "typedef ";
506  }
507 
508  os << type_to_string(unresolved_clean);
509  if(!base_decls.str().empty())
510  {
511  PRECONDITION(language->id()=="cpp");
512  os << ": " << base_decls.str();
513  }
514  os << '\n';
515  os << "{\n";
516  os << struct_body.str();
517 
518  /*
519  if(!struct_type.components().empty())
520  {
521  os << indent << name << "(){}\n";
522  os << indent << "explicit " << name
523  << "(" + constructor_args + ")\n";
524  os << indent << "{\n";
525  os << constructor_body;
526  os << indent << "}\n";
527  }
528  */
529 
530  os << "}";
531  if(type.get_bool(ID_C_transparent_union))
532  os << " __attribute__ ((__transparent_union__))";
533  if(type.get_bool(ID_C_packed))
534  os << " __attribute__ ((__packed__))";
535  if(!typedef_str.empty())
536  os << " " << typedef_str;
537  os << ";\n\n";
538 }
539 
541  const typet &type,
542  std::ostream &os)
543 {
544  PRECONDITION(type.id()==ID_c_enum);
545 
546  const irept &tag=type.find(ID_tag);
547  const irep_idt &name=tag.get(ID_C_base_name);
548 
549  if(tag.is_nil() ||
550  !converted_enum.insert(name).second)
551  return;
552 
553  c_enum_typet enum_type=to_c_enum_type(type);
554  c_enum_typet::memberst &members=
555  (c_enum_typet::memberst &)(enum_type.add(ID_body).get_sub());
556  for(c_enum_typet::memberst::iterator
557  it=members.begin();
558  it!=members.end();
559  ++it)
560  {
561  const irep_idt bn=it->get_base_name();
562 
563  if(declared_enum_constants.find(bn)!=
564  declared_enum_constants.end() ||
566  {
567  std::string new_bn=id2string(name)+"$$"+id2string(bn);
568  it->set_base_name(new_bn);
569  }
570 
572  std::make_pair(bn, it->get_base_name()));
573  }
574 
575  os << type_to_string(enum_type);
576 
577  if(enum_type.get_bool(ID_C_packed))
578  os << " __attribute__ ((__packed__))";
579 
580  os << ";\n\n";
581 }
582 
584  code_declt &decl,
585  std::list<irep_idt> &local_static,
586  std::list<irep_idt> &local_type_decls)
587 {
588  exprt value=nil_exprt();
589 
590  if(decl.operands().size()==2)
591  {
592  value=decl.op1();
593  decl.operands().resize(1);
594  }
595 
596  goto_programt tmp;
598  t->code=decl;
599 
600  if(value.is_not_nil())
601  {
602  t=tmp.add_instruction(ASSIGN);
603  t->code=code_assignt(decl.op0(), value);
604  }
605 
607 
608  std::unordered_set<irep_idt> typedef_names;
609  for(const auto &td : typedef_map)
610  typedef_names.insert(td.first);
611 
612  code_blockt b;
613  goto_program2codet p2s(
614  irep_idt(),
615  tmp,
617  b,
618  local_static,
619  local_type_decls,
620  typedef_names,
622  p2s();
623 
624  POSTCONDITION(b.statements().size() == 1);
625  decl.swap(b.op0());
626 }
627 
633 void dump_ct::collect_typedefs(const typet &type, bool early)
634 {
635  std::unordered_set<irep_idt> deps;
636  collect_typedefs_rec(type, early, deps);
637 }
638 
647  const typet &type,
648  bool early,
649  std::unordered_set<irep_idt> &dependencies)
650 {
652  return;
653 
654  std::unordered_set<irep_idt> local_deps;
655 
656  if(type.id()==ID_code)
657  {
658  const code_typet &code_type=to_code_type(type);
659 
660  collect_typedefs_rec(code_type.return_type(), early, local_deps);
661  for(const auto &param : code_type.parameters())
662  collect_typedefs_rec(param.type(), early, local_deps);
663  }
664  else if(type.id()==ID_pointer || type.id()==ID_array)
665  {
666  collect_typedefs_rec(type.subtype(), early, local_deps);
667  }
668  else if(type.id() == ID_symbol_type)
669  {
670  const symbolt &symbol=
671  ns.lookup(to_symbol_type(type).get_identifier());
672  collect_typedefs_rec(symbol.type, early, local_deps);
673  }
674  else if(
675  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
676  type.id() == ID_union_tag)
677  {
678  const symbolt &symbol = ns.lookup(to_tag_type(type));
679  collect_typedefs_rec(symbol.type, early, local_deps);
680  }
681 
682  const irep_idt &typedef_str=type.get(ID_C_typedef);
683 
684  if(!typedef_str.empty())
685  {
686  std::pair<typedef_mapt::iterator, bool> entry=
687  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
688 
689  if(entry.second ||
690  (early && entry.first->second.type_decl_str.empty()))
691  {
692  if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
693  {
694  system_headers.insert("stdarg.h");
695  early=false;
696  }
697  else
698  {
699  typet t=type;
700  t.remove(ID_C_typedef);
701 
702  std::ostringstream oss;
703  oss << "typedef " << make_decl(typedef_str, t) << ';';
704 
705  entry.first->second.type_decl_str=oss.str();
706  entry.first->second.dependencies=local_deps;
707  }
708  }
709 
710  if(early)
711  {
712  entry.first->second.early=true;
713 
714  for(const auto &d : local_deps)
715  {
716  auto td_entry=typedef_map.find(d);
717  PRECONDITION(td_entry!=typedef_map.end());
718  td_entry->second.early=true;
719  }
720  }
721 
722  dependencies.insert(typedef_str);
723  }
724 
725  dependencies.insert(local_deps.begin(), local_deps.end());
726 }
727 
730 {
731  // sort the symbols first to ensure deterministic replacement in
732  // typedef_types below as there could be redundant declarations
733  // typedef int x;
734  // typedef int y;
735  std::map<std::string, symbolt> symbols_sorted;
736  for(const auto &symbol_entry : copied_symbol_table.symbols)
737  symbols_sorted.insert(
738  {id2string(symbol_entry.first), symbol_entry.second});
739 
740  for(const auto &symbol_entry : symbols_sorted)
741  {
742  const symbolt &symbol=symbol_entry.second;
743 
744  if(symbol.is_macro && symbol.is_type &&
745  symbol.location.get_function().empty())
746  {
747  const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
748  PRECONDITION(!typedef_str.empty());
749  typedef_types[symbol.type]=typedef_str;
751  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
752  else
753  collect_typedefs(symbol.type, false);
754  }
755  }
756 }
757 
760 void dump_ct::dump_typedefs(std::ostream &os) const
761 {
762  // we need to compute a topological sort; we do so by picking all
763  // typedefs the dependencies of which have been emitted into to_insert
764  std::vector<typedef_infot> typedefs_sorted;
765  typedefs_sorted.reserve(typedef_map.size());
766 
767  // elements in to_insert are lexicographically sorted and ready for
768  // output
769  std::map<std::string, typedef_infot> to_insert;
770 
771  std::unordered_set<irep_idt> typedefs_done;
772  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> forward_deps,
773  reverse_deps;
774 
775  for(const auto &td : typedef_map)
776  if(!td.second.type_decl_str.empty())
777  {
778  if(td.second.dependencies.empty())
779  // those can be dumped immediately
780  to_insert.insert({id2string(td.first), td.second});
781  else
782  {
783  // delay them until dependencies are dumped
784  forward_deps.insert({td.first, td.second.dependencies});
785  for(const auto &d : td.second.dependencies)
786  reverse_deps[d].insert(td.first);
787  }
788  }
789 
790  while(!to_insert.empty())
791  {
792  // the topologically next element (lexicographically ranked first
793  // among all the dependencies of which have been dumped)
794  typedef_infot t=to_insert.begin()->second;
795  to_insert.erase(to_insert.begin());
796  // move to the output queue
797  typedefs_sorted.push_back(t);
798 
799  // find any depending typedefs that are now valid, or at least
800  // reduce the remaining dependencies
801  auto r_it=reverse_deps.find(t.typedef_name);
802  if(r_it==reverse_deps.end())
803  continue;
804 
805  // reduce remaining dependencies
806  std::unordered_set<irep_idt> &r_deps = r_it->second;
807  for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
808  it != r_deps.end();) // no ++it
809  {
810  auto f_it=forward_deps.find(*it);
811  if(f_it==forward_deps.end()) // might be done already
812  {
813  it=r_deps.erase(it);
814  continue;
815  }
816 
817  // update dependencies
818  std::unordered_set<irep_idt> &f_deps = f_it->second;
819  PRECONDITION(!f_deps.empty());
820  PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
821  f_deps.erase(t.typedef_name);
822 
823  if(f_deps.empty()) // all depenencies done now!
824  {
825  const auto td_entry=typedef_map.find(*it);
826  PRECONDITION(td_entry!=typedef_map.end());
827  to_insert.insert({id2string(*it), td_entry->second});
828  forward_deps.erase(*it);
829  it=r_deps.erase(it);
830  }
831  else
832  ++it;
833  }
834  }
835 
836  POSTCONDITION(forward_deps.empty());
837 
838  for(const auto &td : typedefs_sorted)
839  os << td.type_decl_str << '\n';
840 
841  if(!typedefs_sorted.empty())
842  os << '\n';
843 }
844 
846  const symbolt &symbol,
847  std::ostream &os,
848  local_static_declst &local_static_decls)
849 {
850  const irep_idt &func=symbol.location.get_function();
851  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
852  !converted_global.insert(symbol.name).second)
853  return;
854 
855  code_declt d(symbol.symbol_expr());
856 
857  find_symbols_sett syms;
858  if(symbol.value.is_not_nil())
859  find_symbols(symbol.value, syms);
860 
861  // add a tentative declaration to cater for symbols in the initializer
862  // relying on it this symbol
863  if((func.empty() || symbol.is_extern) &&
864  (symbol.value.is_nil() || !syms.empty()))
865  {
866  os << "// " << symbol.name << '\n';
867  os << "// " << symbol.location << '\n';
868  os << expr_to_string(d) << '\n';
869  }
870 
871  if(!symbol.value.is_nil())
872  {
873  std::set<std::string> symbols_sorted;
874  for(find_symbols_sett::const_iterator
875  it=syms.begin();
876  it!=syms.end();
877  ++it)
878  {
879  bool inserted=symbols_sorted.insert(id2string(*it)).second;
880  CHECK_RETURN(inserted);
881  }
882 
883  for(std::set<std::string>::const_iterator
884  it=symbols_sorted.begin();
885  it!=symbols_sorted.end();
886  ++it)
887  {
888  const symbolt &sym=ns.lookup(*it);
889  if(!sym.is_type && sym.is_static_lifetime && sym.type.id()!=ID_code)
890  convert_global_variable(sym, os, local_static_decls);
891  }
892 
893  d.copy_to_operands(symbol.value);
894  }
895 
896  if(!func.empty() && !symbol.is_extern)
897  {
898  local_static_decls.emplace(symbol.name, d);
899  }
900  else if(!symbol.value.is_nil())
901  {
902  os << "// " << symbol.name << '\n';
903  os << "// " << symbol.location << '\n';
904 
905  std::list<irep_idt> empty_static, empty_types;
906  cleanup_decl(d, empty_static, empty_types);
907  CHECK_RETURN(empty_static.empty());
908  os << expr_to_string(d) << '\n';
909  }
910 }
911 
916 {
918  code_blockt decls;
919 
920  const symbolt *argc_sym=nullptr;
921  if(!ns.lookup("argc'", argc_sym))
922  {
923  symbol_exprt argc("argc", argc_sym->type);
924  replace.insert(argc_sym->symbol_expr(), argc);
925  code_declt d(argc);
926  decls.add(d);
927  }
928  const symbolt *argv_sym=nullptr;
929  if(!ns.lookup("argv'", argv_sym))
930  {
931  symbol_exprt argv("argv", argv_sym->type);
932  // replace argc' by argc in the type of argv['] to maintain type consistency
933  // while replacing
934  replace(argv);
935  replace.insert(symbol_exprt(argv_sym->name, argv.type()), argv);
936  code_declt d(argv);
937  decls.add(d);
938  }
939  const symbolt *return_sym=nullptr;
940  if(!ns.lookup("return'", return_sym))
941  {
942  symbol_exprt return_value("return_value", return_sym->type);
943  replace.insert(return_sym->symbol_expr(), return_value);
944  code_declt d(return_value);
945  decls.add(d);
946  }
947 
948  for(auto &code : b.statements())
949  {
950  if(code.get_statement()==ID_function_call)
951  {
952  exprt &func=to_code_function_call(code).function();
953  if(func.id()==ID_symbol)
954  {
955  symbol_exprt &s=to_symbol_expr(func);
956  if(s.get_identifier()==ID_main)
958  else if(s.get_identifier() == INITIALIZE_FUNCTION)
959  continue;
960  }
961  }
962 
963  decls.add(code);
964  }
965 
966  b.swap(decls);
967  replace(b);
968 }
969 
971  const symbolt &symbol,
972  const bool skip_main,
973  std::ostream &os_decl,
974  std::ostream &os_body,
975  local_static_declst &local_static_decls)
976 {
977  // don't dump artificial main
978  if(skip_main && symbol.name==goto_functionst::entry_point())
979  return;
980 
981  // convert the goto program back to code - this might change
982  // the function type
983  goto_functionst::function_mapt::const_iterator func_entry=
984  goto_functions.function_map.find(symbol.name);
985  if(func_entry!=goto_functions.function_map.end() &&
986  func_entry->second.body_available())
987  {
988  code_blockt b;
989  std::list<irep_idt> type_decls, local_static;
990 
991  std::unordered_set<irep_idt> typedef_names;
992  for(const auto &td : typedef_map)
993  typedef_names.insert(td.first);
994 
995  goto_program2codet p2s(
996  symbol.name,
997  func_entry->second.body,
999  b,
1000  local_static,
1001  type_decls,
1002  typedef_names,
1003  system_headers);
1004  p2s();
1005 
1007  b,
1008  local_static,
1009  local_static_decls,
1010  type_decls);
1011 
1012  convertedt converted_c_bak(converted_compound);
1013  convertedt converted_e_bak(converted_enum);
1014 
1016  enum_constants_bak(declared_enum_constants);
1017 
1019  b,
1020  type_decls);
1021 
1022  converted_enum.swap(converted_e_bak);
1023  converted_compound.swap(converted_c_bak);
1024 
1025  if(harness && symbol.name==goto_functions.entry_point())
1026  cleanup_harness(b);
1027 
1028  os_body << "// " << symbol.name << '\n';
1029  os_body << "// " << symbol.location << '\n';
1030  if(symbol.name==goto_functions.entry_point())
1031  os_body << make_decl(ID_main, symbol.type) << '\n';
1032  else if(!harness || symbol.name!=ID_main)
1033  os_body << make_decl(symbol.name, symbol.type) << '\n';
1034  else if(harness && symbol.name==ID_main)
1035  {
1036  os_body << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1037  << '\n';
1038  }
1039  os_body << expr_to_string(b);
1040  os_body << "\n\n";
1041 
1042  declared_enum_constants.swap(enum_constants_bak);
1043  }
1044 
1045  if(symbol.name!=goto_functionst::entry_point() &&
1046  symbol.name!=ID_main)
1047  {
1048  os_decl << "// " << symbol.name << '\n';
1049  os_decl << "// " << symbol.location << '\n';
1050  os_decl << make_decl(symbol.name, symbol.type) << ";\n";
1051  }
1052  else if(harness && symbol.name==ID_main)
1053  {
1054  os_decl << "// " << symbol.name << '\n';
1055  os_decl << "// " << symbol.location << '\n';
1056  os_decl << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1057  << ";\n";
1058  }
1059 
1060  // make sure typedef names used in the function declaration are
1061  // available
1062  collect_typedefs(symbol.type, true);
1063 }
1064 
1066  const irep_idt &identifier,
1067  codet &root,
1068  code_blockt* &dest,
1069  exprt::operandst::iterator &before)
1070 {
1071  if(!root.has_operands())
1072  return false;
1073 
1074  code_blockt *our_dest=nullptr;
1075 
1076  exprt::operandst &operands=root.operands();
1077  exprt::operandst::iterator first_found=operands.end();
1078 
1079  Forall_expr(it, operands)
1080  {
1081  bool found=false;
1082 
1083  // be aware of the skip-carries-type hack
1084  if(it->id()==ID_code &&
1085  to_code(*it).get_statement()!=ID_skip)
1087  identifier,
1088  to_code(*it),
1089  our_dest,
1090  before);
1091  else
1092  {
1093  find_symbols_sett syms;
1094  find_type_and_expr_symbols(*it, syms);
1095 
1096  found=syms.find(identifier)!=syms.end();
1097  }
1098 
1099  if(!found)
1100  continue;
1101 
1102  if(!our_dest)
1103  {
1104  // first containing block
1105  if(root.get_statement()==ID_block)
1106  {
1107  dest=&(to_code_block(root));
1108  before=it;
1109  }
1110 
1111  return true;
1112  }
1113  else
1114  {
1115  // there is a containing block and this is the first operand
1116  // that contains identifier
1117  if(first_found==operands.end())
1118  first_found=it;
1119  // we have seen it already - pick the first occurrence in this
1120  // block
1121  else if(root.get_statement()==ID_block)
1122  {
1123  dest=&(to_code_block(root));
1124  before=first_found;
1125 
1126  return true;
1127  }
1128  // we have seen it already - outer block has to deal with this
1129  else
1130  return true;
1131  }
1132  }
1133 
1134  if(first_found!=operands.end())
1135  {
1136  dest=our_dest;
1137 
1138  return true;
1139  }
1140 
1141  return false;
1142 }
1143 
1145  code_blockt &b,
1146  const std::list<irep_idt> &local_static,
1147  local_static_declst &local_static_decls,
1148  std::list<irep_idt> &type_decls)
1149 {
1150  // look up last identifier first as its value may introduce the
1151  // other ones
1152  for(std::list<irep_idt>::const_reverse_iterator
1153  it=local_static.rbegin();
1154  it!=local_static.rend();
1155  ++it)
1156  {
1157  local_static_declst::const_iterator d_it=
1158  local_static_decls.find(*it);
1159  PRECONDITION(d_it!=local_static_decls.end());
1160 
1161  code_declt d=d_it->second;
1162  std::list<irep_idt> redundant;
1163  cleanup_decl(d, redundant, type_decls);
1164 
1165  code_blockt *dest_ptr=nullptr;
1166  exprt::operandst::iterator before=b.operands().end();
1167 
1168  // some use of static variables might be optimised out if it is
1169  // within an if(false) { ... } block
1170  if(find_block_position_rec(*it, b, dest_ptr, before))
1171  {
1172  CHECK_RETURN(dest_ptr!=nullptr);
1173  dest_ptr->operands().insert(before, d);
1174  }
1175  }
1176 }
1177 
1179  code_blockt &b,
1180  const std::list<irep_idt> &type_decls)
1181 {
1182  // look up last identifier first as its value may introduce the
1183  // other ones
1184  for(std::list<irep_idt>::const_reverse_iterator
1185  it=type_decls.rbegin();
1186  it!=type_decls.rend();
1187  ++it)
1188  {
1189  const typet &type=ns.lookup(*it).type;
1190  // feed through plain C to expr2c by ending and re-starting
1191  // a comment block ...
1192  std::ostringstream os_body;
1193  os_body << *it << " */\n";
1194  convert_compound(type, symbol_typet(*it), false, os_body);
1195  os_body << "/*";
1196 
1197  code_skipt skip;
1198  skip.add_source_location().set_comment(os_body.str());
1199  // another hack to ensure symbols inside types are seen
1200  skip.type()=type;
1201 
1202  code_blockt *dest_ptr=nullptr;
1203  exprt::operandst::iterator before=b.operands().end();
1204 
1205  // we might not find it in case a transparent union type cast
1206  // has been removed by cleanup operations
1207  if(find_block_position_rec(*it, b, dest_ptr, before))
1208  {
1209  CHECK_RETURN(dest_ptr!=nullptr);
1210  dest_ptr->operands().insert(before, skip);
1211  }
1212  }
1213 }
1214 
1216 {
1217  Forall_operands(it, expr)
1218  cleanup_expr(*it);
1219 
1220  cleanup_type(expr.type());
1221 
1222  if(expr.id()==ID_struct)
1223  {
1224  struct_typet type=
1225  to_struct_type(ns.follow(expr.type()));
1226 
1227  struct_union_typet::componentst old_components;
1228  old_components.swap(type.components());
1229 
1230  exprt::operandst old_ops;
1231  old_ops.swap(expr.operands());
1232 
1233  PRECONDITION(old_components.size()==old_ops.size());
1234  exprt::operandst::iterator o_it=old_ops.begin();
1235  for(const auto &old_comp : old_components)
1236  {
1237  const bool is_zero_bit_field =
1238  old_comp.type().id() == ID_c_bit_field &&
1239  to_c_bit_field_type(old_comp.type()).get_width() == 0;
1240 
1241  if(!old_comp.get_is_padding() && !is_zero_bit_field)
1242  {
1243  type.components().push_back(old_comp);
1244  expr.move_to_operands(*o_it);
1245  }
1246  ++o_it;
1247  }
1248  expr.type().swap(type);
1249  }
1250  else if(expr.id()==ID_union)
1251  {
1252  union_exprt &u=to_union_expr(expr);
1253  const union_typet &u_type_f=to_union_type(ns.follow(u.type()));
1254 
1255  if(!u.type().get_bool(ID_C_transparent_union) &&
1256  !u_type_f.get_bool(ID_C_transparent_union))
1257  {
1258  if(u_type_f.get_component(u.get_component_name()).get_is_padding())
1259  // we just use an empty struct to fake an empty union
1260  expr=struct_exprt(struct_typet());
1261  }
1262  // add a typecast for NULL
1263  else if(u.op().id()==ID_constant &&
1264  u.op().type().id()==ID_pointer &&
1265  u.op().type().subtype().id()==ID_empty &&
1266  (u.op().is_zero() ||
1267  to_constant_expr(u.op()).get_value()==ID_NULL))
1268  {
1269  const struct_union_typet::componentt &comp=
1270  u_type_f.get_component(u.get_component_name());
1271  const typet &u_op_type=comp.type();
1272  PRECONDITION(u_op_type.id()==ID_pointer);
1273 
1274  typecast_exprt tc(u.op(), u_op_type);
1275  expr.swap(tc);
1276  }
1277  else
1278  {
1279  exprt tmp;
1280  tmp.swap(u.op());
1281  expr.swap(tmp);
1282  }
1283  }
1284  else if(expr.id()==ID_typecast &&
1285  expr.op0().id()==ID_typecast &&
1286  base_type_eq(expr.type(), expr.op0().type(), ns))
1287  {
1288  exprt tmp=expr.op0();
1289  expr.swap(tmp);
1290  }
1291  else if(expr.id()==ID_code &&
1292  to_code(expr).get_statement()==ID_function_call &&
1293  to_code_function_call(to_code(expr)).function().id()==ID_symbol)
1294  {
1296  const symbol_exprt &fn=to_symbol_expr(call.function());
1297  code_function_callt::argumentst &arguments=call.arguments();
1298 
1299  // don't edit function calls we might have introduced
1300  const symbolt *s;
1301  if(!ns.lookup(fn.get_identifier(), s))
1302  {
1303  const symbolt &fn_sym=ns.lookup(fn.get_identifier());
1304  const code_typet &code_type=to_code_type(fn_sym.type);
1305  const code_typet::parameterst &parameters=code_type.parameters();
1306 
1307  if(parameters.size()==arguments.size())
1308  {
1309  code_typet::parameterst::const_iterator it=parameters.begin();
1310  Forall_expr(it2, arguments)
1311  {
1312  const typet &type=ns.follow(it->type());
1313  if(type.id()==ID_union &&
1314  type.get_bool(ID_C_transparent_union))
1315  {
1316  if(it2->id()==ID_typecast &&
1317  base_type_eq(it2->type(), type, ns))
1318  *it2=to_typecast_expr(*it2).op();
1319 
1320  // add a typecast for NULL or 0
1321  if(it2->id()==ID_constant &&
1322  (it2->is_zero() || to_constant_expr(*it2).get_value()==ID_NULL))
1323  {
1324  const typet &comp_type=
1325  to_union_type(type).components().front().type();
1326 
1327  if(comp_type.id()==ID_pointer)
1328  *it2=typecast_exprt(*it2, comp_type);
1329  }
1330  }
1331 
1332  ++it;
1333  }
1334  }
1335  }
1336  }
1337  else if(expr.id()==ID_constant &&
1338  expr.type().id()==ID_signedbv)
1339  {
1340  #if 0
1341  const irep_idt &cformat=expr.get(ID_C_cformat);
1342 
1343  if(!cformat.empty())
1344  {
1345  declared_enum_constants_mapt::const_iterator entry=
1346  declared_enum_constants.find(cformat);
1347 
1348  if(entry!=declared_enum_constants.end() &&
1349  entry->first!=entry->second)
1350  expr.set(ID_C_cformat, entry->second);
1351  else if(entry==declared_enum_constants.end() &&
1352  !std::isdigit(id2string(cformat)[0]))
1353  expr.remove(ID_C_cformat);
1354  }
1355  #endif
1356  }
1357 }
1358 
1360 {
1361  Forall_subtypes(it, type)
1362  cleanup_type(*it);
1363 
1364  if(type.id()==ID_code)
1365  {
1366  code_typet &code_type=to_code_type(type);
1367 
1368  cleanup_type(code_type.return_type());
1369 
1370  for(code_typet::parameterst::iterator
1371  it=code_type.parameters().begin();
1372  it!=code_type.parameters().end();
1373  ++it)
1374  cleanup_type(it->type());
1375  }
1376 
1377  if(type.id()==ID_array)
1378  cleanup_expr(to_array_type(type).size());
1379 
1380  POSTCONDITION(
1381  (type.id()!=ID_union && type.id()!=ID_struct) ||
1382  !type.get(ID_tag).empty());
1383 }
1384 
1385 std::string dump_ct::type_to_string(const typet &type)
1386 {
1387  std::string ret;
1388  typet t=type;
1389  cleanup_type(t);
1390  language->from_type(t, ret, ns);
1391  return ret;
1392 }
1393 
1394 std::string dump_ct::expr_to_string(const exprt &expr)
1395 {
1396  std::string ret;
1397  exprt e=expr;
1398  cleanup_expr(e);
1399  language->from_expr(e, ret, ns);
1400  return ret;
1401 }
1402 
1403 void dump_c(
1404  const goto_functionst &src,
1405  const bool use_system_headers,
1406  const bool use_all_headers,
1407  const bool include_harness,
1408  const namespacet &ns,
1409  std::ostream &out)
1410 {
1411  dump_ct goto2c(
1412  src,
1413  use_system_headers,
1414  use_all_headers,
1415  include_harness,
1416  ns,
1418  out << goto2c;
1419 }
1420 
1422  const goto_functionst &src,
1423  const bool use_system_headers,
1424  const bool use_all_headers,
1425  const bool include_harness,
1426  const namespacet &ns,
1427  std::ostream &out)
1428 {
1429  dump_ct goto2cpp(
1430  src,
1431  use_system_headers,
1432  use_all_headers,
1433  include_harness,
1434  ns,
1436  out << goto2cpp;
1437 }
const irep_idt & get_statement() const
Definition: std_code.h:56
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const bool harness
Definition: dump_c_class.h:53
struct configt::ansi_ct ansi_c
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:633
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
Semantic type conversion.
Definition: std_expr.h:2277
std::unique_ptr< languaget > new_cpp_language()
Base type of functions.
Definition: std_types.h:751
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
void 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:1144
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
const exprt & op() const
Definition: std_expr.h:371
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
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.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
void set_comment(const irep_idt &comment)
declared_enum_constants_mapt declared_enum_constants
Definition: dump_c_class.h:63
const irep_idt & get_function() const
const namespacet ns
Definition: dump_c_class.h:51
const irep_idt & get_identifier() const
Definition: std_expr.h:176
code_operandst & statements()
Definition: std_code.h:159
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1385
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:503
std::ostream & operator<<(std::ostream &out, dump_ct &src)
Definition: dump_c.cpp:28
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::vector< componentt > componentst
Definition: std_types.h:203
std::unordered_map< irep_idt, code_declt > local_static_declst
Definition: dump_c_class.h:131
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
const irep_idt & get_value() const
Definition: std_expr.h:4403
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1394
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
std::vector< parametert > parameterst
Definition: std_types.h:754
exprt value
Initial value of symbol.
Definition: symbol.h:34
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
const componentst & components() const
Definition: std_types.h:205
Dump C from Goto Program.
Dump Goto-Program as C/C++ Source.
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:70
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
exprt::operandst argumentst
Definition: std_code.h:1055
unsignedbv_typet size_type()
Definition: c_types.cpp:58
Symbol table entry.
Definition: symbol.h:27
const goto_functionst & goto_functions
Definition: dump_c_class.h:49
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Structure type, corresponds to C style structs.
Definition: std_types.h:276
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
configt config
Definition: config.cpp:24
#define POSTCONDITION(CONDITION)
Definition: invariant.h:454
bool is_static_lifetime
Definition: symbol.h:65
convertedt converted_enum
Definition: dump_c_class.h:56
std::unordered_set< irep_idt > convertedt
Definition: dump_c_class.h:55
subt & get_sub()
Definition: irep.h:317
static bool find_block_position_rec(const irep_idt &identifier, codet &root, code_blockt *&dest, exprt::operandst::iterator &before)
Definition: dump_c.cpp:1065
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:93
std::string make_decl(const irep_idt &identifier, const typet &type)
Definition: dump_c_class.h:92
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:1403
const irep_idt & id() const
Definition: irep.h:259
typedef_typest typedef_types
Definition: dump_c_class.h:82
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1178
std::size_t long_long_int_width
Definition: config.h:35
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
argumentst & arguments()
Definition: std_code.h:1109
A reference into the symbol table.
Definition: std_types.h:62
instructionst::iterator targett
Definition: goto_program.h:414
Replace expression or type symbols by an expression or type, respectively.
A codet representing the declaration of a local variable.
Definition: std_code.h:352
#define Forall_expr(it, expr)
Definition: expr.h:35
The NIL expression.
Definition: std_expr.h:4461
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1278
std::string main
Definition: config.h:172
#define INITIALIZE_FUNCTION
Union constructor from single element.
Definition: std_expr.h:1840
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
Definition: dump_c.cpp:310
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Definition: dump_c.cpp:583
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
C++ Language Module.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.
Definition: dump_c.cpp:729
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
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...
const exprt & size() const
Definition: std_types.h:1010
system_library_symbolst system_symbols
Definition: dump_c_class.h:60
Base class for tree-like data structures with sharing.
Definition: irep.h:156
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const symbolst & symbols
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
std::set< std::string > system_headers
Definition: dump_c_class.h:58
std::unique_ptr< languaget > language
Definition: dump_c_class.h:52
convertedt converted_global
Definition: dump_c_class.h:56
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
std::size_t get_width() const
Definition: std_types.h:1117
std::unordered_map< irep_idt, irep_idt > declared_enum_constants_mapt
Definition: dump_c_class.h:62
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< exprt > operandst
Definition: expr.h:57
Dump Goto-Program as C/C++ Source.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
bool is_extern
Definition: symbol.h:66
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typedef_mapt typedef_map
Definition: dump_c_class.h:80
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:646
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Definition: dump_c.cpp:296
Base type for structs and unions.
Definition: std_types.h:114
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1215
exprt & function()
Definition: std_code.h:1099
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
The union type.
Definition: std_types.h:425
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
irept & add(const irep_namet &name)
Definition: irep.cpp:305
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
void convert_compound_enum(const typet &type, std::ostream &os)
Definition: dump_c.cpp:540
std::unique_ptr< languaget > new_ansi_c_language()
#define Forall_subtypes(it, type)
Definition: type.h:222
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
void operator()(std::ostream &out)
Definition: dump_c.cpp:34
void swap(irept &irep)
Definition: irep.h:303
irep_idt get_component_name() const
Definition: std_expr.h:1863
#define Forall_operands(it, expr)
Definition: expr.h:26
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
source_locationt & add_source_location()
Definition: expr.h:233
A codet representing sequential composition of program statements.
Definition: std_code.h:150
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
static std::string indent(const unsigned n)
Definition: dump_c_class.h:87
A codet representing a skip statement.
Definition: std_code.h:237
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:1491
Expression to hold a symbol (variable)
Definition: std_expr.h:143
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:970
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void dump_typedefs(std::ostream &os) const
Print all typedefs that are not covered via typedef struct xyz { ...
Definition: dump_c.cpp:760
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:697
dstringt irep_idt
Definition: irep.h:32
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
void remove(const irep_namet &name)
Definition: irep.cpp:269
bool is_type
Definition: symbol.h:61
Base Type Computation.
const typet & subtype() const
Definition: type.h:38
convertedt converted_compound
Definition: dump_c_class.h:56
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
void cleanup_type(typet &type)
Definition: dump_c.cpp:1359
symbol_tablet copied_symbol_table
Definition: dump_c_class.h:50
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
Definition: dump_c.cpp:845
Struct constructor from list of elements.
Definition: std_expr.h:1920
std::vector< c_enum_membert > memberst
Definition: std_types.h:672
bool empty() const
Definition: dstring.h:75
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
void find_symbols(const exprt &src, find_symbols_sett &dest)
The type of C enums.
Definition: std_types.h:647
const typet & return_type() const
Definition: std_types.h:883
bool is_macro
Definition: symbol.h:61
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
void cleanup_harness(code_blockt &b)
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
Definition: dump_c.cpp:915
#define forall_irep(it, irep)
Definition: irep.h:62
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:1421