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