cprover
expr2c.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "expr2c.h"
10 
11 #include <algorithm>
12 #include <cassert>
13 #include <sstream>
14 
15 #include <map>
16 
17 #include <util/arith_tools.h>
18 #include <util/c_types.h>
19 #include <util/config.h>
20 #include <util/cprover_prefix.h>
21 #include <util/find_symbols.h>
22 #include <util/fixedbv.h>
23 #include <util/lispexpr.h>
24 #include <util/lispirep.h>
25 #include <util/namespace.h>
27 #include <util/suffix.h>
28 #include <util/symbol.h>
29 
30 #include "c_misc.h"
31 #include "c_qualifiers.h"
32 #include "expr2c_class.h"
33 
34 // clang-format off
35 
37 {
38  true,
39  true,
40  true,
41  "TRUE",
42  "FALSE"
43 };
44 
46 {
47  false,
48  false,
49  false,
50  "1",
51  "0"
52 };
53 
54 // clang-format on
55 /*
56 
57 Precedences are as follows. Higher values mean higher precedence.
58 
59 16 function call ()
60  ++ -- [] . ->
61 
62 1 comma
63 
64 */
65 
66 irep_idt expr2ct::id_shorthand(const irep_idt &identifier) const
67 {
68  const symbolt *symbol;
69 
70  if(!ns.lookup(identifier, symbol) &&
71  !symbol->base_name.empty() &&
72  has_suffix(id2string(identifier), id2string(symbol->base_name)))
73  return symbol->base_name;
74 
75  std::string sh=id2string(identifier);
76 
77  std::string::size_type pos=sh.rfind("::");
78  if(pos!=std::string::npos)
79  sh.erase(0, pos+2);
80 
81  return sh;
82 }
83 
84 static std::string clean_identifier(const irep_idt &id)
85 {
86  std::string dest=id2string(id);
87 
88  std::string::size_type c_pos=dest.find("::");
89  if(c_pos!=std::string::npos &&
90  dest.rfind("::")==c_pos)
91  dest.erase(0, c_pos+2);
92  else if(c_pos!=std::string::npos)
93  {
94  for(std::string::iterator it2=dest.begin();
95  it2!=dest.end();
96  ++it2)
97  if(*it2==':')
98  *it2='$';
99  else if(*it2=='-')
100  *it2='_';
101  }
102 
103  // rewrite . as used in ELF section names
104  std::replace(dest.begin(), dest.end(), '.', '_');
105 
106  return dest;
107 }
108 
110 {
111  find_symbols_sett symbols;
112  find_symbols(expr, symbols);
113 
114  // avoid renaming parameters, if possible
115  for(find_symbols_sett::const_iterator
116  it=symbols.begin();
117  it!=symbols.end();
118  it++)
119  {
120  const symbolt *symbol;
121  bool is_param=!ns.lookup(*it, symbol) && symbol->is_parameter;
122 
123  if(!is_param)
124  continue;
125 
126  irep_idt sh=id_shorthand(*it);
127 
128  std::string func = id2string(*it);
129  func = func.substr(0, func.rfind("::"));
130 
131  // if there is a global symbol of the same name as the shorthand (even if
132  // not present in this particular expression) then there is a collision
133  const symbolt *global_symbol;
134  if(!ns.lookup(sh, global_symbol))
135  sh = func + "$$" + id2string(sh);
136 
137  ns_collision[func].insert(sh);
138 
139  if(!shorthands.insert(std::make_pair(*it, sh)).second)
140  UNREACHABLE;
141  }
142 
143  for(find_symbols_sett::const_iterator
144  it=symbols.begin();
145  it!=symbols.end();
146  it++)
147  {
148  if(shorthands.find(*it)!=shorthands.end())
149  continue;
150 
151  irep_idt sh=id_shorthand(*it);
152 
153  bool has_collision=
154  ns_collision[irep_idt()].find(sh)!=
155  ns_collision[irep_idt()].end();
156 
157  if(!has_collision)
158  {
159  // if there is a global symbol of the same name as the shorthand (even if
160  // not present in this particular expression) then there is a collision
161  const symbolt *symbol;
162  has_collision=!ns.lookup(sh, symbol);
163  }
164 
165  if(!has_collision)
166  {
167  irep_idt func;
168 
169  const symbolt *symbol;
170  if(!ns.lookup(*it, symbol))
171  func=symbol->location.get_function();
172 
173  has_collision=!ns_collision[func].insert(sh).second;
174  }
175 
176  if(has_collision)
177  sh=clean_identifier(*it);
178 
179  shorthands.insert(std::make_pair(*it, sh));
180  }
181 }
182 
183 std::string expr2ct::convert(const typet &src)
184 {
185  return convert_rec(src, c_qualifierst(), "");
186 }
187 
189  const typet &src,
190  const qualifierst &qualifiers,
191  const std::string &declarator)
192 {
193  std::unique_ptr<qualifierst> clone = qualifiers.clone();
194  c_qualifierst &new_qualifiers = dynamic_cast<c_qualifierst &>(*clone);
195  new_qualifiers.read(src);
196 
197  std::string q=new_qualifiers.as_string();
198 
199  std::string d=
200  declarator==""?declarator:" "+declarator;
201 
202  if(src.find(ID_C_typedef).is_not_nil())
203  {
204  return q+id2string(src.get(ID_C_typedef))+d;
205  }
206 
207  if(src.id()==ID_bool)
208  {
209  return q + CPROVER_PREFIX + "bool" + d;
210  }
211  else if(src.id()==ID_c_bool)
212  {
213  return q+"_Bool"+d;
214  }
215  else if(src.id()==ID_string)
216  {
217  return q + CPROVER_PREFIX + "string" + d;
218  }
219  else if(src.id()==ID_natural ||
220  src.id()==ID_integer ||
221  src.id()==ID_rational)
222  {
223  return q+src.id_string()+d;
224  }
225  else if(src.id()==ID_empty)
226  {
227  return q+"void"+d;
228  }
229  else if(src.id()==ID_complex)
230  {
231  // these take more or less arbitrary subtypes
232  return q+"_Complex "+convert(src.subtype())+d;
233  }
234  else if(src.id()==ID_floatbv)
235  {
236  std::size_t width=to_floatbv_type(src).get_width();
237 
238  if(width==config.ansi_c.single_width)
239  return q+"float"+d;
240  else if(width==config.ansi_c.double_width)
241  return q+"double"+d;
242  else if(width==config.ansi_c.long_double_width)
243  return q+"long double"+d;
244  else
245  {
246  std::string swidth=src.get_string(ID_width);
247  std::string fwidth=src.get_string(ID_f);
248  return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]";
249  }
250  }
251  else if(src.id()==ID_fixedbv)
252  {
253  const std::size_t width=to_fixedbv_type(src).get_width();
254 
255  const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
256  return q + CPROVER_PREFIX + "fixedbv[" + std::to_string(width) + "][" +
257  std::to_string(fraction_bits) + "]" + d;
258  }
259  else if(src.id()==ID_c_bit_field)
260  {
261  std::string width=std::to_string(to_c_bit_field_type(src).get_width());
262  return q+convert(src.subtype())+d+" : "+width;
263  }
264  else if(src.id()==ID_signedbv ||
265  src.id()==ID_unsignedbv)
266  {
267  // annotated?
268  irep_idt c_type=src.get(ID_C_c_type);
269  const std::string c_type_str=c_type_as_string(c_type);
270 
271  if(c_type==ID_char &&
272  config.ansi_c.char_is_unsigned!=(src.id()==ID_unsignedbv))
273  {
274  if(src.id()==ID_signedbv)
275  return q+"signed char"+d;
276  else
277  return q+"unsigned char"+d;
278  }
279  else if(c_type!=ID_wchar_t && !c_type_str.empty())
280  return q+c_type_str+d;
281 
282  // There is also wchar_t among the above, but this isn't a C type.
283 
284  mp_integer width=string2integer(src.get_string(ID_width));
285 
286  bool is_signed=src.id()==ID_signedbv;
287  std::string sign_str=is_signed?"signed ":"unsigned ";
288 
289  if(width==config.ansi_c.int_width)
290  {
291  if(is_signed)
292  sign_str="";
293  return q+sign_str+"int"+d;
294  }
295  else if(width==config.ansi_c.long_int_width)
296  {
297  if(is_signed)
298  sign_str="";
299  return q+sign_str+"long int"+d;
300  }
301  else if(width==config.ansi_c.char_width)
302  {
303  // always include sign
304  return q+sign_str+"char"+d;
305  }
306  else if(width==config.ansi_c.short_int_width)
307  {
308  if(is_signed)
309  sign_str="";
310  return q+sign_str+"short int"+d;
311  }
312  else if(width==config.ansi_c.long_long_int_width)
313  {
314  if(is_signed)
315  sign_str="";
316  return q+sign_str+"long long int"+d;
317  }
318  else if(width==128)
319  {
320  if(is_signed)
321  sign_str="";
322  return q+sign_str+"__int128";
323  }
324  else
325  {
326  return q + sign_str + CPROVER_PREFIX + "bitvector[" +
327  integer2string(width) + "]" + d;
328  }
329  }
330  else if(src.id()==ID_struct)
331  {
332  return convert_struct_type(src, q, d);
333  }
334  else if(src.id()==ID_incomplete_struct)
335  {
336  std::string dest=q+"struct";
337 
338  const std::string &tag=src.get_string(ID_tag);
339  if(tag!="")
340  dest+=" "+tag;
341  dest+=d;
342 
343  return dest;
344  }
345  else if(src.id()==ID_union)
346  {
347  const union_typet &union_type=to_union_type(src);
348 
349  std::string dest=q+"union";
350 
351  const irep_idt &tag=union_type.get_tag();
352  if(tag!="")
353  dest+=" "+id2string(tag);
354  dest+=" {";
355 
356  for(const auto &c : union_type.components())
357  {
358  dest+=' ';
359  dest += convert_rec(c.type(), c_qualifierst(), id2string(c.get_name()));
360  dest+=';';
361  }
362 
363  dest+=" }";
364 
365  dest+=d;
366 
367  return dest;
368  }
369  else if(src.id()==ID_incomplete_union)
370  {
371  std::string dest=q+"union";
372 
373  const std::string &tag=src.get_string(ID_tag);
374  if(tag!="")
375  dest+=" "+tag;
376  dest+=d;
377 
378  return dest;
379  }
380  else if(src.id()==ID_c_enum)
381  {
382  std::string result;
383  result+=q;
384  result+="enum";
385 
386  // do we have a tag?
387  const irept &tag=src.find(ID_tag);
388 
389  if(tag.is_nil())
390  {
391  }
392  else
393  {
394  result+=' ';
395  result+=tag.get_string(ID_C_base_name);
396  }
397 
398  result+=' ';
399  result+='{';
400 
401  // add members
402  const c_enum_typet::memberst &members=to_c_enum_type(src).members();
403 
404  for(c_enum_typet::memberst::const_iterator
405  it=members.begin();
406  it!=members.end();
407  it++)
408  {
409  if(it!=members.begin())
410  result+=',';
411  result+=' ';
412  result+=id2string(it->get_base_name());
413  result+='=';
414  result+=id2string(it->get_value());
415  }
416 
417  result+=" }";
418 
419  result+=d;
420  return result;
421  }
422  else if(src.id()==ID_incomplete_c_enum)
423  {
424  const irept &tag=src.find(ID_tag);
425 
426  if(tag.is_not_nil())
427  {
428  std::string result=q+"enum";
429  result+=" "+tag.get_string(ID_C_base_name);
430  result+=d;
431  return result;
432  }
433  }
434  else if(src.id()==ID_c_enum_tag)
435  {
436  const c_enum_tag_typet &c_enum_tag_type=to_c_enum_tag_type(src);
437  const symbolt &symbol=ns.lookup(c_enum_tag_type);
438  std::string result=q+"enum";
439  result+=" "+id2string(symbol.base_name);
440  result+=d;
441  return result;
442  }
443  else if(src.id()==ID_pointer)
444  {
445  c_qualifierst sub_qualifiers;
446  sub_qualifiers.read(src.subtype());
447  const typet &subtype_followed=ns.follow(src.subtype());
448 
449  // The star gets attached to the declarator.
450  std::string new_declarator="*";
451 
452  if(q!="" &&
453  (!declarator.empty() || subtype_followed.id()==ID_pointer))
454  new_declarator+=" "+q;
455 
456  new_declarator+=declarator;
457 
458  // Depending on precedences, we may add parentheses.
459  if(subtype_followed.id()==ID_code ||
460  (sizeof_nesting==0 &&
461  (subtype_followed.id()==ID_array ||
462  subtype_followed.id()==ID_incomplete_array)))
463  new_declarator="("+new_declarator+")";
464 
465  return convert_rec(src.subtype(), sub_qualifiers, new_declarator);
466  }
467  else if(src.id()==ID_array)
468  {
469  return convert_array_type(src, qualifiers, declarator);
470  }
471  else if(src.id()==ID_incomplete_array)
472  {
473  // The [] gets attached to the declarator.
474  // This won't parse without declarator.
475  return convert_rec(
476  src.subtype(), qualifiers, declarator+"[]");
477  }
478  else if(src.id() == ID_symbol_type)
479  {
480  symbol_typet symbolic_type=to_symbol_type(src);
481  const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
482 
483  // Providing we have a valid identifer, we can just use that rather than
484  // trying to find the concrete type
485  if(typedef_identifer!="")
486  {
487  return q+id2string(typedef_identifer)+d;
488  }
489  else
490  {
491  const typet &followed=ns.follow(src);
492 
493  if(followed.id()==ID_struct)
494  {
495  std::string dest=q+"struct";
496  const irep_idt &tag=to_struct_type(followed).get_tag();
497  if(tag!="")
498  dest+=" "+id2string(tag);
499  dest+=d;
500  return dest;
501  }
502  else if(followed.id()==ID_union)
503  {
504  std::string dest=q+"union";
505  const irep_idt &tag=to_union_type(followed).get_tag();
506  if(tag!="")
507  dest+=" "+id2string(tag);
508  dest+=d;
509  return dest;
510  }
511  else
512  return convert_rec(followed, new_qualifiers, declarator);
513  }
514  }
515  else if(src.id()==ID_struct_tag)
516  {
517  const struct_tag_typet &struct_tag_type=
518  to_struct_tag_type(src);
519 
520  std::string dest=q+"struct";
521  const std::string &tag=ns.follow_tag(struct_tag_type).get_string(ID_tag);
522  if(tag!="")
523  dest+=" "+tag;
524  dest+=d;
525 
526  return dest;
527  }
528  else if(src.id()==ID_union_tag)
529  {
530  const union_tag_typet &union_tag_type=
531  to_union_tag_type(src);
532 
533  std::string dest=q+"union";
534  const std::string &tag=ns.follow_tag(union_tag_type).get_string(ID_tag);
535  if(tag!="")
536  dest+=" "+tag;
537  dest+=d;
538 
539  return dest;
540  }
541  else if(src.id()==ID_code)
542  {
543  const code_typet &code_type=to_code_type(src);
544 
545  // C doesn't really have syntax for function types,
546  // i.e., the following won't parse without declarator
547  std::string dest=declarator+"(";
548 
549  const code_typet::parameterst &parameters=code_type.parameters();
550 
551  if(parameters.empty())
552  {
553  if(code_type.has_ellipsis())
554  dest+=""; // empty!
555  else
556  dest+="void"; // means 'no parameters'
557  }
558  else
559  {
560  for(code_typet::parameterst::const_iterator
561  it=parameters.begin();
562  it!=parameters.end();
563  it++)
564  {
565  if(it!=parameters.begin())
566  dest+=", ";
567 
568  if(it->get_identifier().empty())
569  dest+=convert(it->type());
570  else
571  {
572  std::string arg_declarator=
573  convert(symbol_exprt(it->get_identifier(), it->type()));
574  dest+=convert_rec(it->type(), c_qualifierst(), arg_declarator);
575  }
576  }
577 
578  if(code_type.has_ellipsis())
579  dest+=", ...";
580  }
581 
582  dest+=')';
583 
584  c_qualifierst ret_qualifiers;
585  ret_qualifiers.read(code_type.return_type());
586  // _Noreturn should go with the return type
587  if(new_qualifiers.is_noreturn)
588  {
589  ret_qualifiers.is_noreturn=true;
590  new_qualifiers.is_noreturn=false;
591  q=new_qualifiers.as_string();
592  }
593 
594  const typet &return_type=code_type.return_type();
595 
596  // return type may be a function pointer or array
597  const typet *non_ptr_type=&ns.follow(return_type);
598  while(non_ptr_type->id()==ID_pointer)
599  non_ptr_type=&(ns.follow(non_ptr_type->subtype()));
600 
601  if(non_ptr_type->id()==ID_code ||
602  non_ptr_type->id()==ID_array)
603  dest=convert_rec(return_type, ret_qualifiers, dest);
604  else
605  dest=convert_rec(return_type, ret_qualifiers, "")+" "+dest;
606 
607  if(!q.empty())
608  {
609  dest+=" "+q;
610  // strip trailing space off q
611  if(dest[dest.size()-1]==' ')
612  dest.resize(dest.size()-1);
613  }
614 
615  return dest;
616  }
617  else if(src.id()==ID_vector)
618  {
619  const vector_typet &vector_type=to_vector_type(src);
620 
621  const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
622  std::string dest="__gcc_v"+integer2string(size_int);
623 
624  std::string tmp=convert(vector_type.subtype());
625 
626  if(tmp=="signed char" || tmp=="char")
627  dest+="qi";
628  else if(tmp=="signed short int")
629  dest+="hi";
630  else if(tmp=="signed int")
631  dest+="si";
632  else if(tmp=="signed long long int")
633  dest+="di";
634  else if(tmp=="float")
635  dest+="sf";
636  else if(tmp=="double")
637  dest+="df";
638  else
639  {
640  const std::string subtype=convert(vector_type.subtype());
641  dest=subtype;
642  dest+=" __attribute__((vector_size (";
643  dest+=convert(vector_type.size());
644  dest+="*sizeof("+subtype+"))))";
645  }
646 
647  return q+dest+d;
648  }
649  else if(src.id()==ID_gcc_builtin_va_list)
650  {
651  return q+"__builtin_va_list"+d;
652  }
653  else if(src.id()==ID_constructor ||
654  src.id()==ID_destructor)
655  {
656  return q+"__attribute__(("+id2string(src.id())+")) void"+d;
657  }
658 
659  {
660  lispexprt lisp;
661  irep2lisp(src, lisp);
662  std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
663  dest+=d;
664 
665  return dest;
666  }
667 }
668 
676  const typet &src,
677  const std::string &qualifiers_str,
678  const std::string &declarator_str)
679 {
680  return convert_struct_type(
681  src,
682  qualifiers_str,
683  declarator_str,
686 }
687 
699  const typet &src,
700  const std::string &qualifiers,
701  const std::string &declarator,
702  bool inc_struct_body,
703  bool inc_padding_components)
704 {
705  // Either we are including the body (in which case it makes sense to include
706  // or exclude the parameters) or there is no body so therefore we definitely
707  // shouldn't be including the parameters
708  assert(inc_struct_body || !inc_padding_components);
709 
710  const struct_typet &struct_type=to_struct_type(src);
711 
712  std::string dest=qualifiers+"struct";
713 
714  const irep_idt &tag=struct_type.get_tag();
715  if(tag!="")
716  dest+=" "+id2string(tag);
717 
718  if(inc_struct_body)
719  {
720  dest+=" {";
721 
722  for(const auto &component : struct_type.components())
723  {
724  // Skip padding parameters unless we including them
725  if(component.get_is_padding() && !inc_padding_components)
726  {
727  continue;
728  }
729 
730  dest+=' ';
731  dest+=convert_rec(
732  component.type(),
733  c_qualifierst(),
734  id2string(component.get_name()));
735  dest+=';';
736  }
737 
738  dest+=" }";
739  }
740 
741  dest+=declarator;
742 
743  return dest;
744 }
745 
753  const typet &src,
754  const qualifierst &qualifiers,
755  const std::string &declarator_str)
756 {
757  return convert_array_type(
758  src, qualifiers, declarator_str, configuration.include_array_size);
759 }
760 
770  const typet &src,
771  const qualifierst &qualifiers,
772  const std::string &declarator_str,
773  bool inc_size_if_possible)
774 {
775  // The [...] gets attached to the declarator.
776  std::string array_suffix;
777 
778  if(to_array_type(src).size().is_nil() || !inc_size_if_possible)
779  array_suffix="[]";
780  else
781  array_suffix="["+convert(to_array_type(src).size())+"]";
782 
783  // This won't really parse without declarator.
784  // Note that qualifiers are passed down.
785  return convert_rec(
786  src.subtype(), qualifiers, declarator_str+array_suffix);
787 }
788 
790  const typecast_exprt &src,
791  unsigned &precedence)
792 {
793  if(src.operands().size()!=1)
794  return convert_norep(src, precedence);
795 
796  // some special cases
797 
798  const typet &to_type=ns.follow(src.type());
799  const typet &from_type=ns.follow(src.op().type());
800 
801  if(to_type.id()==ID_c_bool &&
802  from_type.id()==ID_bool)
803  return convert_with_precedence(src.op(), precedence);
804 
805  if(to_type.id()==ID_bool &&
806  from_type.id()==ID_c_bool)
807  return convert_with_precedence(src.op(), precedence);
808 
809  std::string dest="("+convert(src.type())+")";
810 
811  unsigned p;
812  std::string tmp=convert_with_precedence(src.op(), p);
813 
814  if(precedence>p)
815  dest+='(';
816  dest+=tmp;
817  if(precedence>p)
818  dest+=')';
819 
820  return dest;
821 }
822 
824  const exprt &src,
825  const std::string &symbol1,
826  const std::string &symbol2,
827  unsigned precedence)
828 {
829  if(src.operands().size()!=3)
830  return convert_norep(src, precedence);
831 
832  const exprt &op0=src.op0();
833  const exprt &op1=src.op1();
834  const exprt &op2=src.op2();
835 
836  unsigned p0, p1, p2;
837 
838  std::string s_op0=convert_with_precedence(op0, p0);
839  std::string s_op1=convert_with_precedence(op1, p1);
840  std::string s_op2=convert_with_precedence(op2, p2);
841 
842  std::string dest;
843 
844  if(precedence>=p0)
845  dest+='(';
846  dest+=s_op0;
847  if(precedence>=p0)
848  dest+=')';
849 
850  dest+=' ';
851  dest+=symbol1;
852  dest+=' ';
853 
854  if(precedence>=p1)
855  dest+='(';
856  dest+=s_op1;
857  if(precedence>=p1)
858  dest+=')';
859 
860  dest+=' ';
861  dest+=symbol2;
862  dest+=' ';
863 
864  if(precedence>=p2)
865  dest+='(';
866  dest+=s_op2;
867  if(precedence>=p2)
868  dest+=')';
869 
870  return dest;
871 }
872 
874  const exprt &src,
875  const std::string &symbol,
876  unsigned precedence)
877 {
878  if(src.operands().size()!=2)
879  return convert_norep(src, precedence);
880 
881  unsigned p0, p1;
882 
883  std::string op0=convert_with_precedence(src.op0(), p0);
884  std::string op1=convert_with_precedence(src.op1(), p1);
885 
886  std::string dest=symbol+" { ";
887  dest+=convert(src.op0().type());
888  dest+=" "+op0+"; ";
889  dest+=op1;
890  dest+=" }";
891 
892  return dest;
893 }
894 
896  const exprt &src,
897  unsigned precedence)
898 {
899  if(src.operands().size()<3)
900  return convert_norep(src, precedence);
901 
902  unsigned p0;
903  std::string op0=convert_with_precedence(src.op0(), p0);
904 
905  std::string dest;
906 
907  if(precedence>p0)
908  dest+='(';
909  dest+=op0;
910  if(precedence>p0)
911  dest+=')';
912 
913  dest+=" WITH [";
914 
915  for(size_t i=1; i<src.operands().size(); i+=2)
916  {
917  std::string op1, op2;
918  unsigned p1, p2;
919 
920  if(i!=1)
921  dest+=", ";
922 
923  if(src.operands()[i].id()==ID_member_name)
924  {
925  const irep_idt &component_name=
926  src.operands()[i].get(ID_component_name);
927 
928  const typet &full_type=ns.follow(src.op0().type());
929 
930  const struct_union_typet &struct_union_type=
931  to_struct_union_type(full_type);
932 
933  const struct_union_typet::componentt &comp_expr=
934  struct_union_type.get_component(component_name);
935 
936  assert(comp_expr.is_not_nil());
937 
938  irep_idt display_component_name;
939 
940  if(comp_expr.get_pretty_name().empty())
941  display_component_name=component_name;
942  else
943  display_component_name=comp_expr.get_pretty_name();
944 
945  op1="."+id2string(display_component_name);
946  p1=10;
947  }
948  else
949  op1=convert_with_precedence(src.operands()[i], p1);
950 
951  op2=convert_with_precedence(src.operands()[i+1], p2);
952 
953  dest+=op1;
954  dest+=":=";
955  dest+=op2;
956  }
957 
958  dest+=']';
959 
960  return dest;
961 }
962 
964  const let_exprt &src,
965  unsigned precedence)
966 {
967  if(src.operands().size()<3)
968  return convert_norep(src, precedence);
969 
970  unsigned p0;
971  std::string op0=convert_with_precedence(src.op0(), p0);
972 
973  std::string dest="LET ";
974  dest+=convert(src.symbol());
975  dest+='=';
976  dest+=convert(src.value());
977  dest+=" IN ";
978  dest+=convert(src.where());
979 
980  return dest;
981 }
982 
984  const exprt &src,
985  unsigned precedence)
986 {
987  // needs exactly 3 operands
988  if(src.operands().size()!=3)
989  return convert_norep(src, precedence);
990 
991  std::string dest;
992 
993  dest+="UPDATE(";
994 
995  std::string op0, op1, op2;
996  unsigned p0, p2;
997 
998  op0=convert_with_precedence(src.op0(), p0);
999  op2=convert_with_precedence(src.op2(), p2);
1000 
1001  if(precedence>p0)
1002  dest+='(';
1003  dest+=op0;
1004  if(precedence>p0)
1005  dest+=')';
1006 
1007  dest+=", ";
1008 
1009  const exprt &designator=src.op1();
1010 
1011  forall_operands(it, designator)
1012  dest+=convert(*it);
1013 
1014  dest+=", ";
1015 
1016  if(precedence>p2)
1017  dest+='(';
1018  dest+=op2;
1019  if(precedence>p2)
1020  dest+=')';
1021 
1022  dest+=')';
1023 
1024  return dest;
1025 }
1026 
1028  const exprt &src,
1029  unsigned precedence)
1030 {
1031  if(src.operands().size()<2)
1032  return convert_norep(src, precedence);
1033 
1034  bool condition=true;
1035 
1036  std::string dest="cond {\n";
1037 
1038  forall_operands(it, src)
1039  {
1040  unsigned p;
1041  std::string op=convert_with_precedence(*it, p);
1042 
1043  if(condition)
1044  dest+=" ";
1045 
1046  dest+=op;
1047 
1048  if(condition)
1049  dest+=": ";
1050  else
1051  dest+=";\n";
1052 
1053  condition=!condition;
1054  }
1055 
1056  dest+="} ";
1057 
1058  return dest;
1059 }
1060 
1062  const exprt &src,
1063  const std::string &symbol,
1064  unsigned precedence,
1065  bool full_parentheses)
1066 {
1067  if(src.operands().size()!=2)
1068  return convert_norep(src, precedence);
1069 
1070  const exprt &op0=src.op0();
1071  const exprt &op1=src.op1();
1072 
1073  unsigned p0, p1;
1074 
1075  std::string s_op0=convert_with_precedence(op0, p0);
1076  std::string s_op1=convert_with_precedence(op1, p1);
1077 
1078  std::string dest;
1079 
1080  // In pointer arithmetic, x+(y-z) is unfortunately
1081  // not the same as (x+y)-z, even though + and -
1082  // have the same precedence. We thus add parentheses
1083  // for the case x+(y-z). Similarly, (x*y)/z is not
1084  // the same as x*(y/z), but * and / have the same
1085  // precedence.
1086 
1087  bool use_parentheses0=
1088  precedence>p0 ||
1089  (precedence==p0 && full_parentheses) ||
1090  (precedence==p0 && src.id()!=op0.id());
1091 
1092  if(use_parentheses0)
1093  dest+='(';
1094  dest+=s_op0;
1095  if(use_parentheses0)
1096  dest+=')';
1097 
1098  dest+=' ';
1099  dest+=symbol;
1100  dest+=' ';
1101 
1102  bool use_parentheses1=
1103  precedence>p1 ||
1104  (precedence==p1 && full_parentheses) ||
1105  (precedence==p1 && src.id()!=op1.id());
1106 
1107  if(use_parentheses1)
1108  dest+='(';
1109  dest+=s_op1;
1110  if(use_parentheses1)
1111  dest+=')';
1112 
1113  return dest;
1114 }
1115 
1117  const exprt &src,
1118  const std::string &symbol,
1119  unsigned precedence,
1120  bool full_parentheses)
1121 {
1122  if(src.operands().size()<2)
1123  return convert_norep(src, precedence);
1124 
1125  std::string dest;
1126  bool first=true;
1127 
1128  forall_operands(it, src)
1129  {
1130  if(first)
1131  first=false;
1132  else
1133  {
1134  if(symbol!=", ")
1135  dest+=' ';
1136  dest+=symbol;
1137  dest+=' ';
1138  }
1139 
1140  unsigned p;
1141  std::string op=convert_with_precedence(*it, p);
1142 
1143  // In pointer arithmetic, x+(y-z) is unfortunately
1144  // not the same as (x+y)-z, even though + and -
1145  // have the same precedence. We thus add parentheses
1146  // for the case x+(y-z). Similarly, (x*y)/z is not
1147  // the same as x*(y/z), but * and / have the same
1148  // precedence.
1149 
1150  bool use_parentheses=
1151  precedence>p ||
1152  (precedence==p && full_parentheses) ||
1153  (precedence==p && src.id()!=it->id());
1154 
1155  if(use_parentheses)
1156  dest+='(';
1157  dest+=op;
1158  if(use_parentheses)
1159  dest+=')';
1160  }
1161 
1162  return dest;
1163 }
1164 
1166  const exprt &src,
1167  const std::string &symbol,
1168  unsigned precedence)
1169 {
1170  if(src.operands().size()!=1)
1171  return convert_norep(src, precedence);
1172 
1173  unsigned p;
1174  std::string op=convert_with_precedence(src.op0(), p);
1175 
1176  std::string dest=symbol;
1177  if(precedence>=p ||
1178  (!symbol.empty() && has_prefix(op, symbol)))
1179  dest+='(';
1180  dest+=op;
1181  if(precedence>=p ||
1182  (!symbol.empty() && has_prefix(op, symbol)))
1183  dest+=')';
1184 
1185  return dest;
1186 }
1187 
1188 std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
1189 {
1190  if(src.operands().size() != 2)
1191  return convert_norep(src, precedence);
1192 
1193  unsigned p0;
1194  std::string op0 = convert_with_precedence(src.op0(), p0);
1195 
1196  unsigned p1;
1197  std::string op1 = convert_with_precedence(src.op1(), p1);
1198 
1199  std::string dest = "ALLOCATE";
1200  dest += '(';
1201 
1202  if(src.type().id()==ID_pointer &&
1203  src.type().subtype().id()!=ID_empty)
1204  {
1205  dest+=convert(src.type().subtype());
1206  dest+=", ";
1207  }
1208 
1209  dest += op0 + ", " + op1;
1210  dest += ')';
1211 
1212  return dest;
1213 }
1214 
1216  const exprt &src,
1217  unsigned &precedence)
1218 {
1219  if(!src.operands().empty())
1220  return convert_norep(src, precedence);
1221 
1222  return "NONDET("+convert(src.type())+")";
1223 }
1224 
1226  const exprt &src,
1227  unsigned &precedence)
1228 {
1229  if(src.operands().size()!=1 ||
1230  to_code(src.op0()).get_statement()!=ID_block)
1231  return convert_norep(src, precedence);
1232 
1233  return "("+convert_code(to_code_block(to_code(src.op0())), 0)+")";
1234 }
1235 
1237  const exprt &src,
1238  unsigned &precedence)
1239 {
1240  if(src.operands().size()==1)
1241  return "COIN("+convert(src.op0())+")";
1242  else
1243  return convert_norep(src, precedence);
1244 }
1245 
1247  const exprt &src,
1248  unsigned &precedence)
1249 {
1250  return "L("+src.get_string(ID_literal)+")";
1251 }
1252 
1254  const exprt &src,
1255  unsigned &precedence)
1256 {
1257  if(src.operands().size()==1)
1258  return "PROB_UNIFORM("+convert(src.type())+","+convert(src.op0())+")";
1259  else
1260  return convert_norep(src, precedence);
1261 }
1262 
1264  const exprt &src,
1265  const std::string &name,
1266  unsigned precedence)
1267 {
1268  std::string dest=name;
1269  dest+='(';
1270 
1271  forall_operands(it, src)
1272  {
1273  unsigned p;
1274  std::string op=convert_with_precedence(*it, p);
1275 
1276  if(it!=src.operands().begin())
1277  dest+=", ";
1278 
1279  dest+=op;
1280  }
1281 
1282  dest+=')';
1283 
1284  return dest;
1285 }
1286 
1288  const exprt &src,
1289  unsigned precedence)
1290 {
1291  if(src.operands().size()!=2)
1292  return convert_norep(src, precedence);
1293 
1294  unsigned p0;
1295  std::string op0=convert_with_precedence(src.op0(), p0);
1296  if(*op0.rbegin()==';')
1297  op0.resize(op0.size()-1);
1298 
1299  unsigned p1;
1300  std::string op1=convert_with_precedence(src.op1(), p1);
1301  if(*op1.rbegin()==';')
1302  op1.resize(op1.size()-1);
1303 
1304  std::string dest=op0;
1305  dest+=", ";
1306  dest+=op1;
1307 
1308  return dest;
1309 }
1310 
1312  const exprt &src,
1313  unsigned precedence)
1314 {
1315  if(src.operands().size()==2 &&
1316  src.op0().is_zero() &&
1317  src.op1().id()==ID_constant)
1318  {
1319  // This is believed to be gcc only; check if this is sensible
1320  // in MSC mode.
1321  return convert_with_precedence(src.op1(), precedence)+"i";
1322  }
1323 
1324  // ISO C11 offers:
1325  // double complex CMPLX(double x, double y);
1326  // float complex CMPLXF(float x, float y);
1327  // long double complex CMPLXL(long double x, long double y);
1328 
1329  const typet &subtype=
1330  ns.follow(ns.follow(src.type()).subtype());
1331 
1332  std::string name;
1333 
1334  if(subtype==double_type())
1335  name="CMPLX";
1336  else if(subtype==float_type())
1337  name="CMPLXF";
1338  else if(subtype==long_double_type())
1339  name="CMPLXL";
1340  else
1341  name="CMPLX"; // default, possibly wrong
1342 
1343  std::string dest=name;
1344  dest+='(';
1345 
1346  forall_operands(it, src)
1347  {
1348  unsigned p;
1349  std::string op=convert_with_precedence(*it, p);
1350 
1351  if(it!=src.operands().begin())
1352  dest+=", ";
1353 
1354  dest+=op;
1355  }
1356 
1357  dest+=')';
1358 
1359  return dest;
1360 }
1361 
1363  const exprt &src,
1364  unsigned precedence)
1365 {
1366  if(src.operands().size()!=1)
1367  return convert_norep(src, precedence);
1368 
1369  return "ARRAY_OF("+convert(src.op0())+')';
1370 }
1371 
1373  const exprt &src,
1374  unsigned precedence)
1375 {
1376  if(src.operands().size()!=2)
1377  return convert_norep(src, precedence);
1378 
1379  unsigned p0;
1380  std::string op0=convert_with_precedence(src.op0(), p0);
1381 
1382  unsigned p1;
1383  std::string op1=convert_with_precedence(src.op1(), p1);
1384 
1385  std::string dest=src.id_string();
1386  dest+='(';
1387  dest+=op0;
1388  dest+=", ";
1389  dest+=op1;
1390  dest+=", ";
1391  dest+=convert(src.type());
1392  dest+=')';
1393 
1394  return dest;
1395 }
1396 
1398  const exprt &src,
1399  unsigned precedence)
1400 {
1401  if(src.operands().size()!=3)
1402  return convert_norep(src, precedence);
1403 
1404  unsigned p0;
1405  std::string op0=convert_with_precedence(src.op0(), p0);
1406 
1407  unsigned p1;
1408  std::string op1=convert_with_precedence(src.op1(), p1);
1409 
1410  unsigned p2;
1411  std::string op2=convert_with_precedence(src.op2(), p2);
1412 
1413  std::string dest=src.id_string();
1414  dest+='(';
1415  dest+=op0;
1416  dest+=", ";
1417  dest+=op1;
1418  dest+=", ";
1419  dest+=op2;
1420  dest+=", ";
1421  dest+=convert(src.op2().type());
1422  dest+=')';
1423 
1424  return dest;
1425 }
1426 
1428  const exprt &src,
1429  const std::string &symbol,
1430  unsigned precedence)
1431 {
1432  if(src.operands().size()!=1)
1433  return convert_norep(src, precedence);
1434 
1435  unsigned p;
1436  std::string op=convert_with_precedence(src.op0(), p);
1437 
1438  std::string dest;
1439  if(precedence>p)
1440  dest+='(';
1441  dest+=op;
1442  if(precedence>p)
1443  dest+=')';
1444  dest+=symbol;
1445 
1446  return dest;
1447 }
1448 
1450  const exprt &src,
1451  unsigned precedence)
1452 {
1453  if(src.operands().size()!=2)
1454  return convert_norep(src, precedence);
1455 
1456  unsigned p;
1457  std::string op=convert_with_precedence(src.op0(), p);
1458 
1459  std::string dest;
1460  if(precedence>p)
1461  dest+='(';
1462  dest+=op;
1463  if(precedence>p)
1464  dest+=')';
1465 
1466  dest+='[';
1467  dest+=convert(src.op1());
1468  dest+=']';
1469 
1470  return dest;
1471 }
1472 
1474  const exprt &src, unsigned &precedence)
1475 {
1476  if(src.operands().size()!=2)
1477  return convert_norep(src, precedence);
1478 
1479  std::string dest="POINTER_ARITHMETIC(";
1480 
1481  unsigned p;
1482  std::string op;
1483 
1484  op=convert(src.op0().type());
1485  dest+=op;
1486 
1487  dest+=", ";
1488 
1489  op=convert_with_precedence(src.op0(), p);
1490  if(precedence>p)
1491  dest+='(';
1492  dest+=op;
1493  if(precedence>p)
1494  dest+=')';
1495 
1496  dest+=", ";
1497 
1498  op=convert_with_precedence(src.op1(), p);
1499  if(precedence>p)
1500  dest+='(';
1501  dest+=op;
1502  if(precedence>p)
1503  dest+=')';
1504 
1505  dest+=')';
1506 
1507  return dest;
1508 }
1509 
1511  const exprt &src, unsigned &precedence)
1512 {
1513  if(src.operands().size()!=2)
1514  return convert_norep(src, precedence);
1515 
1516  std::string dest="POINTER_DIFFERENCE(";
1517 
1518  unsigned p;
1519  std::string op;
1520 
1521  op=convert(src.op0().type());
1522  dest+=op;
1523 
1524  dest+=", ";
1525 
1526  op=convert_with_precedence(src.op0(), p);
1527  if(precedence>p)
1528  dest+='(';
1529  dest+=op;
1530  if(precedence>p)
1531  dest+=')';
1532 
1533  dest+=", ";
1534 
1535  op=convert_with_precedence(src.op1(), p);
1536  if(precedence>p)
1537  dest+='(';
1538  dest+=op;
1539  if(precedence>p)
1540  dest+=')';
1541 
1542  dest+=')';
1543 
1544  return dest;
1545 }
1546 
1548 {
1549  unsigned precedence;
1550 
1551  if(!src.operands().empty())
1552  return convert_norep(src, precedence);
1553 
1554  return "."+src.get_string(ID_component_name);
1555 }
1556 
1558 {
1559  unsigned precedence;
1560 
1561  if(src.operands().size()!=1)
1562  return convert_norep(src, precedence);
1563 
1564  return "["+convert(src.op0())+"]";
1565 }
1566 
1568  const member_exprt &src,
1569  unsigned precedence)
1570 {
1571  if(src.operands().size()!=1)
1572  return convert_norep(src, precedence);
1573 
1574  unsigned p;
1575  std::string dest;
1576 
1577  if(src.op0().id()==ID_dereference &&
1578  src.operands().size()==1)
1579  {
1580  std::string op=convert_with_precedence(src.op0().op0(), p);
1581 
1582  if(precedence>p || src.op0().op0().id()==ID_typecast)
1583  dest+='(';
1584  dest+=op;
1585  if(precedence>p || src.op0().op0().id()==ID_typecast)
1586  dest+=')';
1587 
1588  dest+="->";
1589  }
1590  else
1591  {
1592  std::string op=convert_with_precedence(src.op0(), p);
1593 
1594  if(precedence>p || src.op0().id()==ID_typecast)
1595  dest+='(';
1596  dest+=op;
1597  if(precedence>p || src.op0().id()==ID_typecast)
1598  dest+=')';
1599 
1600  dest+='.';
1601  }
1602 
1603  const typet &full_type=ns.follow(src.op0().type());
1604 
1605  if(full_type.id()!=ID_struct &&
1606  full_type.id()!=ID_union)
1607  return convert_norep(src, precedence);
1608 
1609  const struct_union_typet &struct_union_type=
1610  to_struct_union_type(full_type);
1611 
1612  irep_idt component_name=src.get_component_name();
1613 
1614  if(component_name!="")
1615  {
1616  const exprt comp_expr=
1617  struct_union_type.get_component(component_name);
1618 
1619  if(comp_expr.is_nil())
1620  return convert_norep(src, precedence);
1621 
1622  if(!comp_expr.get(ID_pretty_name).empty())
1623  dest+=comp_expr.get_string(ID_pretty_name);
1624  else
1625  dest+=id2string(component_name);
1626 
1627  return dest;
1628  }
1629 
1630  std::size_t n=src.get_component_number();
1631 
1632  if(n>=struct_union_type.components().size())
1633  return convert_norep(src, precedence);
1634 
1635  const exprt comp_expr=
1636  struct_union_type.components()[n];
1637 
1638  dest+=comp_expr.get_string(ID_pretty_name);
1639 
1640  return dest;
1641 }
1642 
1644  const exprt &src,
1645  unsigned precedence)
1646 {
1647  if(src.operands().size()!=1)
1648  return convert_norep(src, precedence);
1649 
1650  return "[]="+convert(src.op0());
1651 }
1652 
1654  const exprt &src,
1655  unsigned precedence)
1656 {
1657  if(src.operands().size()!=1)
1658  return convert_norep(src, precedence);
1659 
1660  return "."+src.get_string(ID_name)+"="+convert(src.op0());
1661 }
1662 
1664  const exprt &src,
1665  unsigned &precedence)
1666 {
1667  lispexprt lisp;
1668  irep2lisp(src, lisp);
1669  std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
1670  precedence=16;
1671  return dest;
1672 }
1673 
1675  const exprt &src,
1676  unsigned &precedence)
1677 {
1678  const irep_idt &id=src.get(ID_identifier);
1679  std::string dest;
1680 
1681  if(src.operands().size()==1 &&
1682  src.op0().id()==ID_predicate_passive_symbol)
1683  dest=src.op0().get_string(ID_identifier);
1684  else
1685  {
1686  std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1687  shorthands.find(id);
1688  // we might be called from conversion of a type
1689  if(entry==shorthands.end())
1690  {
1691  get_shorthands(src);
1692 
1693  entry=shorthands.find(id);
1694  assert(entry!=shorthands.end());
1695  }
1696 
1697  dest=id2string(entry->second);
1698 
1699  #if 0
1700  if(has_prefix(id2string(id), "symex_dynamic::dynamic_object"))
1701  {
1702  if(sizeof_nesting++ == 0)
1703  dest+=" /*"+convert(src.type());
1704  if(--sizeof_nesting == 0)
1705  dest+="*/";
1706  }
1707  #endif
1708  }
1709 
1710  if(src.id()==ID_next_symbol)
1711  dest="NEXT("+dest+")";
1712 
1713  return dest;
1714 }
1715 
1717  const nondet_symbol_exprt &src,
1718  unsigned &precedence)
1719 {
1720  const irep_idt id=src.get_identifier();
1721  return "nondet_symbol("+id2string(id)+")";
1722 }
1723 
1725  const exprt &src,
1726  unsigned &precedence)
1727 {
1728  const std::string &id=src.get_string(ID_identifier);
1729  return "ps("+id+")";
1730 }
1731 
1733  const exprt &src,
1734  unsigned &precedence)
1735 {
1736  const std::string &id=src.get_string(ID_identifier);
1737  return "pns("+id+")";
1738 }
1739 
1741  const exprt &src,
1742  unsigned &precedence)
1743 {
1744  const std::string &id=src.get_string(ID_identifier);
1745  return "pps("+id+")";
1746 }
1747 
1749  const exprt &src,
1750  unsigned &precedence)
1751 {
1752  const std::string &id=src.get_string(ID_identifier);
1753  return id;
1754 }
1755 
1757  const exprt &src,
1758  unsigned &precedence)
1759 {
1760  return "nondet_bool()";
1761 }
1762 
1764  const exprt &src,
1765  unsigned &precedence)
1766 {
1767  if(src.operands().size()!=2)
1768  return convert_norep(src, precedence);
1769 
1770  std::string result="<";
1771 
1772  result+=convert(src.op0());
1773  result+=", ";
1774  result+=convert(src.op1());
1775  result+=", ";
1776 
1777  if(src.type().is_nil())
1778  result+='?';
1779  else
1780  result+=convert(src.type());
1781 
1782  result+='>';
1783 
1784  return result;
1785 }
1786 
1788  const constant_exprt &src,
1789  unsigned &precedence)
1790 {
1791  const irep_idt &base=src.get(ID_C_base);
1792  const typet &type=ns.follow(src.type());
1793  const irep_idt value=src.get_value();
1794  std::string dest;
1795 
1796  if(type.id()==ID_integer ||
1797  type.id()==ID_natural ||
1798  type.id()==ID_rational)
1799  {
1800  dest=id2string(value);
1801  }
1802  else if(type.id()==ID_c_enum ||
1803  type.id()==ID_c_enum_tag)
1804  {
1805  typet c_enum_type=
1806  type.id()==ID_c_enum?to_c_enum_type(type):
1808 
1809  if(c_enum_type.id()!=ID_c_enum)
1810  return convert_norep(src, precedence);
1811 
1812  const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
1813  const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
1814 
1815  mp_integer int_value = bvrep2integer(value, width, is_signed);
1816  mp_integer i=0;
1817 
1818  irep_idt int_value_string=integer2string(int_value);
1819 
1820  const c_enum_typet::memberst &members=
1821  to_c_enum_type(c_enum_type).members();
1822 
1823  for(c_enum_typet::memberst::const_iterator
1824  it=members.begin();
1825  it!=members.end();
1826  it++)
1827  {
1828  if(it->get_value()==int_value_string)
1829  return "/*enum*/"+id2string(it->get_base_name());
1830  }
1831 
1832  // failed...
1833  return "/*enum*/"+integer2string(int_value);
1834  }
1835  else if(type.id()==ID_rational)
1836  return convert_norep(src, precedence);
1837  else if(type.id()==ID_bv)
1838  {
1839  // not C
1840  dest=id2string(value);
1841  }
1842  else if(type.id()==ID_bool)
1843  {
1844  dest=convert_constant_bool(src.is_true());
1845  }
1846  else if(type.id()==ID_unsignedbv ||
1847  type.id()==ID_signedbv ||
1848  type.id()==ID_c_bit_field ||
1849  type.id()==ID_c_bool)
1850  {
1851  const auto width = to_bitvector_type(type).get_width();
1852 
1853  mp_integer int_value =
1854  bvrep2integer(value, width, type.id() == ID_signedbv);
1855 
1856  const irep_idt &c_type=
1857  type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
1858  type.get(ID_C_c_type);
1859 
1860  if(type.id()==ID_c_bool)
1861  {
1862  dest=convert_constant_bool(int_value!=0);
1863  }
1864  else if(type==char_type() &&
1865  type!=signed_int_type() &&
1866  type!=unsigned_int_type())
1867  {
1868  if(int_value=='\n')
1869  dest+="'\\n'";
1870  else if(int_value=='\r')
1871  dest+="'\\r'";
1872  else if(int_value=='\t')
1873  dest+="'\\t'";
1874  else if(int_value=='\'')
1875  dest+="'\\''";
1876  else if(int_value=='\\')
1877  dest+="'\\\\'";
1878  else if(int_value>=' ' && int_value<126)
1879  {
1880  dest+='\'';
1881  dest+=static_cast<char>(integer2ulong(int_value));
1882  dest+='\'';
1883  }
1884  else
1885  dest=integer2string(int_value);
1886  }
1887  else
1888  {
1889  if(base=="16")
1890  dest="0x"+integer2string(int_value, 16);
1891  else if(base=="8")
1892  dest="0"+integer2string(int_value, 8);
1893  else if(base=="2")
1894  dest="0b"+integer2string(int_value, 2);
1895  else
1896  dest=integer2string(int_value);
1897 
1898  if(c_type==ID_unsigned_int)
1899  dest+='u';
1900  else if(c_type==ID_unsigned_long_int)
1901  dest+="ul";
1902  else if(c_type==ID_signed_long_int)
1903  dest+='l';
1904  else if(c_type==ID_unsigned_long_long_int)
1905  dest+="ull";
1906  else if(c_type==ID_signed_long_long_int)
1907  dest+="ll";
1908 
1909  if(src.find(ID_C_c_sizeof_type).is_not_nil() &&
1910  sizeof_nesting==0)
1911  {
1912  const exprt sizeof_expr = build_sizeof_expr(to_constant_expr(src), ns);
1913 
1914  if(sizeof_expr.is_not_nil())
1915  {
1916  ++sizeof_nesting;
1917  dest=convert(sizeof_expr)+" /*"+dest+"*/ ";
1918  --sizeof_nesting;
1919  }
1920  }
1921  }
1922  }
1923  else if(type.id()==ID_floatbv)
1924  {
1926 
1927  if(dest!="" && isdigit(dest[dest.size()-1]))
1928  {
1929  if(dest.find('.')==std::string::npos)
1930  dest+=".0";
1931 
1932  // ANSI-C: double is default; float/long-double require annotation
1933  if(src.type()==float_type())
1934  dest+='f';
1935  else if(src.type()==long_double_type() &&
1937  dest+='l';
1938  }
1939  else if(dest.size()==4 &&
1940  (dest[0]=='+' || dest[0]=='-'))
1941  {
1942  if(dest=="+inf")
1943  dest="+INFINITY";
1944  else if(dest=="-inf")
1945  dest="-INFINITY";
1946  else if(dest=="+NaN")
1947  dest="+NAN";
1948  else if(dest=="-NaN")
1949  dest="-NAN";
1950  }
1951  }
1952  else if(type.id()==ID_fixedbv)
1953  {
1955 
1956  if(dest!="" && isdigit(dest[dest.size()-1]))
1957  {
1958  if(src.type()==float_type())
1959  dest+='f';
1960  else if(src.type()==long_double_type())
1961  dest+='l';
1962  }
1963  }
1964  else if(type.id()==ID_array ||
1965  type.id()==ID_incomplete_array)
1966  {
1967  dest=convert_array(src, precedence);
1968  }
1969  else if(type.id()==ID_pointer)
1970  {
1971  if(value==ID_NULL)
1972  {
1973  dest="NULL";
1974  if(type.subtype().id()!=ID_empty)
1975  dest="(("+convert(type)+")"+dest+")";
1976  }
1977  else if(value==std::string(value.size(), '0') &&
1979  {
1980  dest="NULL";
1981  if(type.subtype().id()!=ID_empty)
1982  dest="(("+convert(type)+")"+dest+")";
1983  }
1984  else
1985  {
1986  // we prefer the annotation
1987  if(src.operands().size()!=1)
1988  return convert_norep(src, precedence);
1989 
1990  if(src.op0().id()==ID_constant)
1991  {
1992  const irep_idt &op_value=src.op0().get(ID_value);
1993 
1994  if(op_value=="INVALID" ||
1995  has_prefix(id2string(op_value), "INVALID-") ||
1996  op_value=="NULL+offset")
1997  dest=id2string(op_value);
1998  else
1999  return convert_norep(src, precedence);
2000  }
2001  else
2002  return convert_with_precedence(src.op0(), precedence);
2003  }
2004  }
2005  else if(type.id()==ID_string)
2006  {
2007  return '"'+id2string(src.get_value())+'"';
2008  }
2009  else
2010  return convert_norep(src, precedence);
2011 
2012  return dest;
2013 }
2014 
2019 std::string expr2ct::convert_constant_bool(bool boolean_value)
2020 {
2021  if(boolean_value)
2022  return configuration.true_string;
2023  else
2024  return configuration.false_string;
2025 }
2026 
2028  const exprt &src,
2029  unsigned &precedence)
2030 {
2031  return convert_struct(
2033 }
2034 
2044  const exprt &src,
2045  unsigned &precedence,
2046  bool include_padding_components)
2047 {
2048  const typet full_type=ns.follow(src.type());
2049 
2050  if(full_type.id()!=ID_struct)
2051  return convert_norep(src, precedence);
2052 
2053  const struct_typet &struct_type=
2054  to_struct_type(full_type);
2055 
2056  const struct_typet::componentst &components=
2057  struct_type.components();
2058 
2059  if(components.size()!=src.operands().size())
2060  return convert_norep(src, precedence);
2061 
2062  std::string dest="{ ";
2063 
2064  exprt::operandst::const_iterator o_it=src.operands().begin();
2065 
2066  bool first=true;
2067  bool newline=false;
2068  size_t last_size=0;
2069 
2070  for(const auto &component : struct_type.components())
2071  {
2072  if(o_it->type().id()==ID_code)
2073  continue;
2074 
2075  if(component.get_is_padding() && !include_padding_components)
2076  {
2077  ++o_it;
2078  continue;
2079  }
2080 
2081  if(first)
2082  first=false;
2083  else
2084  {
2085  dest+=',';
2086 
2087  if(newline)
2088  dest+="\n ";
2089  else
2090  dest+=' ';
2091  }
2092 
2093  std::string tmp=convert(*o_it);
2094 
2095  if(last_size+40<dest.size())
2096  {
2097  newline=true;
2098  last_size=dest.size();
2099  }
2100  else
2101  newline=false;
2102 
2103  dest+='.';
2104  dest+=component.get_string(ID_name);
2105  dest+='=';
2106  dest+=tmp;
2107 
2108  o_it++;
2109  }
2110 
2111  dest+=" }";
2112 
2113  return dest;
2114 }
2115 
2117  const exprt &src,
2118  unsigned &precedence)
2119 {
2120  const typet full_type=ns.follow(src.type());
2121 
2122  if(full_type.id()!=ID_vector)
2123  return convert_norep(src, precedence);
2124 
2125  std::string dest="{ ";
2126 
2127  bool first=true;
2128  bool newline=false;
2129  size_t last_size=0;
2130 
2131  forall_operands(it, src)
2132  {
2133  if(first)
2134  first=false;
2135  else
2136  {
2137  dest+=',';
2138 
2139  if(newline)
2140  dest+="\n ";
2141  else
2142  dest+=' ';
2143  }
2144 
2145  std::string tmp=convert(*it);
2146 
2147  if(last_size+40<dest.size())
2148  {
2149  newline=true;
2150  last_size=dest.size();
2151  }
2152  else
2153  newline=false;
2154 
2155  dest+=tmp;
2156  }
2157 
2158  dest+=" }";
2159 
2160  return dest;
2161 }
2162 
2164  const exprt &src,
2165  unsigned &precedence)
2166 {
2167  std::string dest="{ ";
2168 
2169  if(src.operands().size()!=1)
2170  return convert_norep(src, precedence);
2171 
2172  std::string tmp=convert(src.op0());
2173 
2174  dest+='.';
2175  dest+=src.get_string(ID_component_name);
2176  dest+='=';
2177  dest+=tmp;
2178 
2179  dest+=" }";
2180 
2181  return dest;
2182 }
2183 
2185  const exprt &src,
2186  unsigned &precedence)
2187 {
2188  std::string dest;
2189 
2190  // we treat arrays of characters as string constants,
2191  // and arrays of wchar_t as wide strings
2192 
2193  const typet &subtype=ns.follow(ns.follow(src.type()).subtype());
2194 
2195  bool all_constant=true;
2196 
2197  forall_operands(it, src)
2198  if(!it->is_constant())
2199  all_constant=false;
2200 
2201  if(src.get_bool(ID_C_string_constant) &&
2202  all_constant &&
2203  (subtype==char_type() || subtype==wchar_t_type()))
2204  {
2205  bool wide=subtype==wchar_t_type();
2206 
2207  if(wide)
2208  dest+='L';
2209 
2210  dest+="\"";
2211 
2212  dest.reserve(dest.size()+1+src.operands().size());
2213 
2214  bool last_was_hex=false;
2215 
2216  forall_operands(it, src)
2217  {
2218  // these have a trailing zero
2219  if(it==--src.operands().end())
2220  break;
2221 
2222  const unsigned int ch = numeric_cast_v<unsigned>(*it);
2223 
2224  if(last_was_hex)
2225  {
2226  // we use "string splicing" to avoid ambiguity
2227  if(isxdigit(ch))
2228  dest+="\" \"";
2229 
2230  last_was_hex=false;
2231  }
2232 
2233  switch(ch)
2234  {
2235  case '\n': dest+="\\n"; break; /* NL (0x0a) */
2236  case '\t': dest+="\\t"; break; /* HT (0x09) */
2237  case '\v': dest+="\\v"; break; /* VT (0x0b) */
2238  case '\b': dest+="\\b"; break; /* BS (0x08) */
2239  case '\r': dest+="\\r"; break; /* CR (0x0d) */
2240  case '\f': dest+="\\f"; break; /* FF (0x0c) */
2241  case '\a': dest+="\\a"; break; /* BEL (0x07) */
2242  case '\\': dest+="\\\\"; break;
2243  case '"': dest+="\\\""; break;
2244 
2245  default:
2246  if(ch>=' ' && ch!=127 && ch<0xff)
2247  dest+=static_cast<char>(ch);
2248  else
2249  {
2250  std::ostringstream oss;
2251  oss << "\\x" << std::hex << ch;
2252  dest += oss.str();
2253  last_was_hex=true;
2254  }
2255  }
2256  }
2257 
2258  dest+="\"";
2259 
2260  return dest;
2261  }
2262 
2263  dest="{ ";
2264 
2265  forall_operands(it, src)
2266  {
2267  std::string tmp;
2268 
2269  if(it->is_not_nil())
2270  tmp=convert(*it);
2271 
2272  if((it+1)!=src.operands().end())
2273  {
2274  tmp+=", ";
2275  if(tmp.size()>40)
2276  tmp+="\n ";
2277  }
2278 
2279  dest+=tmp;
2280  }
2281 
2282  dest+=" }";
2283 
2284  return dest;
2285 }
2286 
2288  const exprt &src,
2289  unsigned &precedence)
2290 {
2291  std::string dest="{ ";
2292 
2293  if((src.operands().size()%2)!=0)
2294  return convert_norep(src, precedence);
2295 
2296  forall_operands(it, src)
2297  {
2298  std::string tmp1=convert(*it);
2299 
2300  it++;
2301 
2302  std::string tmp2=convert(*it);
2303 
2304  std::string tmp="["+tmp1+"]="+tmp2;
2305 
2306  if((it+1)!=src.operands().end())
2307  {
2308  tmp+=", ";
2309  if(tmp.size()>40)
2310  tmp+="\n ";
2311  }
2312 
2313  dest+=tmp;
2314  }
2315 
2316  dest+=" }";
2317 
2318  return dest;
2319 }
2320 
2322  const exprt &src,
2323  unsigned &precedence)
2324 {
2325  std::string dest;
2326  if(src.id()!=ID_compound_literal)
2327  dest+="{ ";
2328 
2329  forall_operands(it, src)
2330  {
2331  std::string tmp=convert(*it);
2332 
2333  if((it+1)!=src.operands().end())
2334  {
2335  tmp+=", ";
2336  if(tmp.size()>40)
2337  tmp+="\n ";
2338  }
2339 
2340  dest+=tmp;
2341  }
2342 
2343  if(src.id()!=ID_compound_literal)
2344  dest+=" }";
2345 
2346  return dest;
2347 }
2348 
2350  const exprt &src,
2351  unsigned &precedence)
2352 {
2353  if(src.operands().size()!=1)
2354  {
2355  unsigned precedence;
2356  return convert_norep(src, precedence);
2357  }
2358 
2359  std::string dest=".";
2360  // TODO it->find(ID_member)
2361  dest+='=';
2362  dest+=convert(src.op0());
2363 
2364  return dest;
2365 }
2366 
2368  const function_application_exprt &src,
2369  unsigned &precedence)
2370 {
2371  std::string dest;
2372 
2373  {
2374  unsigned p;
2375  std::string function_str=convert_with_precedence(src.function(), p);
2376  dest+=function_str;
2377  }
2378 
2379  dest+='(';
2380 
2381  forall_expr(it, src.arguments())
2382  {
2383  unsigned p;
2384  std::string arg_str=convert_with_precedence(*it, p);
2385 
2386  if(it!=src.arguments().begin())
2387  dest+=", ";
2388  // TODO: ggf. Klammern je nach p
2389  dest+=arg_str;
2390  }
2391 
2392  dest+=')';
2393 
2394  return dest;
2395 }
2396 
2399  unsigned &precedence)
2400 {
2401  std::string dest;
2402 
2403  {
2404  unsigned p;
2405  std::string function_str=convert_with_precedence(src.function(), p);
2406  dest+=function_str;
2407  }
2408 
2409  dest+='(';
2410 
2411  forall_expr(it, src.arguments())
2412  {
2413  unsigned p;
2414  std::string arg_str=convert_with_precedence(*it, p);
2415 
2416  if(it!=src.arguments().begin())
2417  dest+=", ";
2418  // TODO: ggf. Klammern je nach p
2419  dest+=arg_str;
2420  }
2421 
2422  dest+=')';
2423 
2424  return dest;
2425 }
2426 
2428  const exprt &src,
2429  unsigned &precedence)
2430 {
2431  precedence=16;
2432 
2433  std::string dest="overflow(\"";
2434  dest+=src.id().c_str()+9;
2435  dest+="\"";
2436 
2437  if(!src.operands().empty())
2438  {
2439  dest+=", ";
2440  dest+=convert(src.op0().type());
2441  }
2442 
2443  forall_operands(it, src)
2444  {
2445  unsigned p;
2446  std::string arg_str=convert_with_precedence(*it, p);
2447 
2448  dest+=", ";
2449  // TODO: ggf. Klammern je nach p
2450  dest+=arg_str;
2451  }
2452 
2453  dest+=')';
2454 
2455  return dest;
2456 }
2457 
2458 std::string expr2ct::indent_str(unsigned indent)
2459 {
2460  return std::string(indent, ' ');
2461 }
2462 
2464  const code_asmt &src,
2465  unsigned indent)
2466 {
2467  std::string dest=indent_str(indent);
2468 
2469  if(src.get_flavor()==ID_gcc)
2470  {
2471  if(src.operands().size()==5)
2472  {
2473  dest+="asm(";
2474  dest+=convert(src.op0());
2475  if(!src.operands()[1].operands().empty() ||
2476  !src.operands()[2].operands().empty() ||
2477  !src.operands()[3].operands().empty() ||
2478  !src.operands()[4].operands().empty())
2479  {
2480  // need extended syntax
2481 
2482  // outputs
2483  dest+=" : ";
2484  forall_operands(it, src.op1())
2485  {
2486  if(it->operands().size()==2)
2487  {
2488  if(it!=src.op1().operands().begin())
2489  dest+=", ";
2490  dest+=convert(it->op0());
2491  dest+="(";
2492  dest+=convert(it->op1());
2493  dest+=")";
2494  }
2495  }
2496 
2497  // inputs
2498  dest+=" : ";
2499  forall_operands(it, src.op2())
2500  {
2501  if(it->operands().size()==2)
2502  {
2503  if(it!=src.op2().operands().begin())
2504  dest+=", ";
2505  dest+=convert(it->op0());
2506  dest+="(";
2507  dest+=convert(it->op1());
2508  dest+=")";
2509  }
2510  }
2511 
2512  // clobbered registers
2513  dest+=" : ";
2514  forall_operands(it, src.op3())
2515  {
2516  if(it!=src.op3().operands().begin())
2517  dest+=", ";
2518  if(it->id()==ID_gcc_asm_clobbered_register)
2519  dest+=convert(it->op0());
2520  else
2521  dest+=convert(*it);
2522  }
2523  }
2524  dest+=");";
2525  }
2526  }
2527  else if(src.get_flavor()==ID_msc)
2528  {
2529  if(src.operands().size()==1)
2530  {
2531  dest+="__asm {\n";
2532  dest+=indent_str(indent);
2533  dest+=convert(src.op0());
2534  dest+="\n}";
2535  }
2536  }
2537 
2538  return dest;
2539 }
2540 
2542  const code_whilet &src,
2543  unsigned indent)
2544 {
2545  if(src.operands().size()!=2)
2546  {
2547  unsigned precedence;
2548  return convert_norep(src, precedence);
2549  }
2550 
2551  std::string dest=indent_str(indent);
2552  dest+="while("+convert(src.cond());
2553 
2554  if(src.body().is_nil())
2555  dest+=");";
2556  else
2557  {
2558  dest+=")\n";
2559  dest+=convert_code(
2560  src.body(),
2561  src.body().get_statement()==ID_block ? indent : indent+2);
2562  }
2563 
2564  return dest;
2565 }
2566 
2568  const code_dowhilet &src,
2569  unsigned indent)
2570 {
2571  if(src.operands().size()!=2)
2572  {
2573  unsigned precedence;
2574  return convert_norep(src, precedence);
2575  }
2576 
2577  std::string dest=indent_str(indent);
2578 
2579  if(src.body().is_nil())
2580  dest+="do;";
2581  else
2582  {
2583  dest+="do\n";
2584  dest+=convert_code(
2585  src.body(),
2586  src.body().get_statement()==ID_block ? indent : indent+2);
2587  dest+="\n";
2588  dest+=indent_str(indent);
2589  }
2590 
2591  dest+="while("+convert(src.cond())+");";
2592 
2593  return dest;
2594 }
2595 
2597  const code_ifthenelset &src,
2598  unsigned indent)
2599 {
2600  if(src.operands().size()!=3)
2601  {
2602  unsigned precedence;
2603  return convert_norep(src, precedence);
2604  }
2605 
2606  std::string dest=indent_str(indent);
2607  dest+="if("+convert(src.cond())+")\n";
2608 
2609  if(src.then_case().is_nil())
2610  {
2611  dest+=indent_str(indent+2);
2612  dest+=';';
2613  }
2614  else
2615  dest += convert_code(
2616  src.then_case(),
2617  src.then_case().get_statement() == ID_block ? indent : indent + 2);
2618  dest+="\n";
2619 
2620  if(!src.else_case().is_nil())
2621  {
2622  dest+="\n";
2623  dest+=indent_str(indent);
2624  dest+="else\n";
2625  dest += convert_code(
2626  src.else_case(),
2627  src.else_case().get_statement() == ID_block ? indent : indent + 2);
2628  }
2629 
2630  return dest;
2631 }
2632 
2634  const codet &src,
2635  unsigned indent)
2636 {
2637  if(!src.operands().empty() &&
2638  src.operands().size()!=1)
2639  {
2640  unsigned precedence;
2641  return convert_norep(src, precedence);
2642  }
2643 
2644  std::string dest=indent_str(indent);
2645  dest+="return";
2646 
2647  if(to_code_return(src).has_return_value())
2648  dest+=" "+convert(src.op0());
2649 
2650  dest+=';';
2651 
2652  return dest;
2653 }
2654 
2656  const codet &src,
2657  unsigned indent)
2658 {
2659  std:: string dest=indent_str(indent);
2660  dest+="goto ";
2661  dest+=clean_identifier(src.get(ID_destination));
2662  dest+=';';
2663 
2664  return dest;
2665 }
2666 
2668  const codet &src,
2669  unsigned indent)
2670 {
2671  std::string dest=indent_str(indent);
2672  dest+="break";
2673  dest+=';';
2674 
2675  return dest;
2676 }
2677 
2679  const codet &src,
2680  unsigned indent)
2681 {
2682  if(src.operands().empty())
2683  {
2684  unsigned precedence;
2685  return convert_norep(src, precedence);
2686  }
2687 
2688  std::string dest=indent_str(indent);
2689  dest+="switch(";
2690  dest+=convert(src.op0());
2691  dest+=")\n";
2692 
2693  dest+=indent_str(indent);
2694  dest+='{';
2695 
2696  forall_operands(it, src)
2697  {
2698  if(it==src.operands().begin())
2699  continue;
2700  const exprt &op=*it;
2701 
2702  if(op.get(ID_statement)!=ID_block)
2703  {
2704  unsigned precedence;
2705  dest+=convert_norep(op, precedence);
2706  }
2707  else
2708  {
2709  forall_operands(it2, op)
2710  dest+=convert_code(to_code(*it2), indent+2);
2711  }
2712  }
2713 
2714  dest+="\n";
2715  dest+=indent_str(indent);
2716  dest+='}';
2717 
2718  return dest;
2719 }
2720 
2722  const codet &src,
2723  unsigned indent)
2724 {
2725  std::string dest=indent_str(indent);
2726  dest+="continue";
2727  dest+=';';
2728 
2729  return dest;
2730 }
2731 
2733  const codet &src,
2734  unsigned indent)
2735 {
2736  // initializer to go away
2737  if(src.operands().size()!=1 &&
2738  src.operands().size()!=2)
2739  {
2740  unsigned precedence;
2741  return convert_norep(src, precedence);
2742  }
2743 
2744  std::string declarator=convert(src.op0());
2745 
2746  std::string dest=indent_str(indent);
2747 
2748  const symbolt *symbol=nullptr;
2749  if(!ns.lookup(to_symbol_expr(src.op0()).get_identifier(), symbol))
2750  {
2751  if(symbol->is_file_local &&
2752  (src.op0().type().id()==ID_code || symbol->is_static_lifetime))
2753  dest+="static ";
2754  else if(symbol->is_extern)
2755  dest+="extern ";
2756  else if(
2758  {
2759  dest += "__declspec(dllexport) ";
2760  }
2761 
2762  if(symbol->type.id()==ID_code &&
2763  to_code_type(symbol->type).get_inlined())
2764  dest+="inline ";
2765  }
2766 
2767  dest+=convert_rec(src.op0().type(), c_qualifierst(), declarator);
2768 
2769  if(src.operands().size()==2)
2770  dest+="="+convert(src.op1());
2771 
2772  dest+=';';
2773 
2774  return dest;
2775 }
2776 
2778  const codet &src,
2779  unsigned indent)
2780 {
2781  // initializer to go away
2782  if(src.operands().size()!=1)
2783  {
2784  unsigned precedence;
2785  return convert_norep(src, precedence);
2786  }
2787 
2788  return indent_str(indent) + "dead " + convert(src.op0()) + ";";
2789 }
2790 
2792  const code_fort &src,
2793  unsigned indent)
2794 {
2795  if(src.operands().size()!=4)
2796  {
2797  unsigned precedence;
2798  return convert_norep(src, precedence);
2799  }
2800 
2801  std::string dest=indent_str(indent);
2802  dest+="for(";
2803 
2804  if(!src.init().is_nil())
2805  dest += convert(src.init());
2806  else
2807  dest+=' ';
2808  dest+="; ";
2809  if(!src.cond().is_nil())
2810  dest += convert(src.cond());
2811  dest+="; ";
2812  if(!src.iter().is_nil())
2813  dest += convert(src.iter());
2814 
2815  if(src.body().is_nil())
2816  dest+=");\n";
2817  else
2818  {
2819  dest+=")\n";
2820  dest+=convert_code(
2821  src.body(),
2822  src.body().get_statement()==ID_block ? indent : indent+2);
2823  }
2824 
2825  return dest;
2826 }
2827 
2829  const code_blockt &src,
2830  unsigned indent)
2831 {
2832  std::string dest=indent_str(indent);
2833  dest+="{\n";
2834 
2835  for(const auto &statement : src.statements())
2836  {
2837  if(statement.get_statement() == ID_label)
2838  dest += convert_code(statement, indent);
2839  else
2840  dest += convert_code(statement, indent + 2);
2841 
2842  dest+="\n";
2843  }
2844 
2845  dest+=indent_str(indent);
2846  dest+='}';
2847 
2848  return dest;
2849 }
2850 
2852  const codet &src,
2853  unsigned indent)
2854 {
2855  std::string dest;
2856 
2857  forall_operands(it, src)
2858  {
2859  dest+=convert_code(to_code(*it), indent);
2860  dest+="\n";
2861  }
2862 
2863  return dest;
2864 }
2865 
2867  const codet &src,
2868  unsigned indent)
2869 {
2870  std::string dest=indent_str(indent);
2871 
2872  std::string expr_str;
2873  if(src.operands().size()==1)
2874  expr_str=convert(src.op0());
2875  else
2876  {
2877  unsigned precedence;
2878  expr_str=convert_norep(src, precedence);
2879  }
2880 
2881  dest+=expr_str;
2882  if(dest.empty() || *dest.rbegin()!=';')
2883  dest+=';';
2884 
2885  return dest;
2886 }
2887 
2889  const codet &src,
2890  unsigned indent)
2891 {
2892  static bool comment_done=false;
2893 
2894  if(!comment_done && !src.source_location().get_comment().empty())
2895  {
2896  comment_done=true;
2897  std::string dest=indent_str(indent);
2898  dest+="/* "+id2string(src.source_location().get_comment())+" */\n";
2899  dest+=convert_code(src, indent);
2900  comment_done=false;
2901  return dest;
2902  }
2903 
2904  const irep_idt &statement=src.get_statement();
2905 
2906  if(statement==ID_expression)
2907  return convert_code_expression(src, indent);
2908 
2909  if(statement==ID_block)
2910  return convert_code_block(to_code_block(src), indent);
2911 
2912  if(statement==ID_switch)
2913  return convert_code_switch(src, indent);
2914 
2915  if(statement==ID_for)
2916  return convert_code_for(to_code_for(src), indent);
2917 
2918  if(statement==ID_while)
2919  return convert_code_while(to_code_while(src), indent);
2920 
2921  if(statement==ID_asm)
2922  return convert_code_asm(to_code_asm(src), indent);
2923 
2924  if(statement==ID_skip)
2925  return indent_str(indent)+";";
2926 
2927  if(statement==ID_dowhile)
2928  return convert_code_dowhile(to_code_dowhile(src), indent);
2929 
2930  if(statement==ID_ifthenelse)
2931  return convert_code_ifthenelse(to_code_ifthenelse(src), indent);
2932 
2933  if(statement==ID_return)
2934  return convert_code_return(src, indent);
2935 
2936  if(statement==ID_goto)
2937  return convert_code_goto(src, indent);
2938 
2939  if(statement==ID_printf)
2940  return convert_code_printf(src, indent);
2941 
2942  if(statement==ID_fence)
2943  return convert_code_fence(src, indent);
2944 
2945  if(statement==ID_input)
2946  return convert_code_input(src, indent);
2947 
2948  if(statement==ID_output)
2949  return convert_code_output(src, indent);
2950 
2951  if(statement==ID_assume)
2952  return convert_code_assume(src, indent);
2953 
2954  if(statement==ID_assert)
2955  return convert_code_assert(src, indent);
2956 
2957  if(statement==ID_break)
2958  return convert_code_break(src, indent);
2959 
2960  if(statement==ID_continue)
2961  return convert_code_continue(src, indent);
2962 
2963  if(statement==ID_decl)
2964  return convert_code_decl(src, indent);
2965 
2966  if(statement==ID_decl_block)
2967  return convert_code_decl_block(src, indent);
2968 
2969  if(statement==ID_dead)
2970  return convert_code_dead(src, indent);
2971 
2972  if(statement==ID_assign)
2973  return convert_code_assign(to_code_assign(src), indent);
2974 
2975  if(statement=="lock")
2976  return convert_code_lock(src, indent);
2977 
2978  if(statement=="unlock")
2979  return convert_code_unlock(src, indent);
2980 
2981  if(statement==ID_atomic_begin)
2982  return indent_str(indent) + CPROVER_PREFIX + "atomic_begin();";
2983 
2984  if(statement==ID_atomic_end)
2985  return indent_str(indent) + CPROVER_PREFIX + "atomic_end();";
2986 
2987  if(statement==ID_function_call)
2989 
2990  if(statement==ID_label)
2991  return convert_code_label(to_code_label(src), indent);
2992 
2993  if(statement==ID_switch_case)
2994  return convert_code_switch_case(to_code_switch_case(src), indent);
2995 
2996  if(statement==ID_array_set)
2997  return convert_code_array_set(src, indent);
2998 
2999  if(statement==ID_array_copy)
3000  return convert_code_array_copy(src, indent);
3001 
3002  if(statement==ID_array_replace)
3003  return convert_code_array_replace(src, indent);
3004 
3005  if(statement=="set_may" ||
3006  statement=="set_must")
3007  return
3008  indent_str(indent)+convert_function(src, id2string(statement), 16)+";";
3009 
3010  unsigned precedence;
3011  return convert_norep(src, precedence);
3012 }
3013 
3015  const code_assignt &src,
3016  unsigned indent)
3017 {
3018  std::string tmp=convert_binary(src, "=", 2, true);
3019 
3020  std::string dest=indent_str(indent)+tmp+";";
3021 
3022  return dest;
3023 }
3024 
3026  const codet &src,
3027  unsigned indent)
3028 {
3029  if(src.operands().size()!=1)
3030  {
3031  unsigned precedence;
3032  return convert_norep(src, precedence);
3033  }
3034 
3035  return indent_str(indent)+"LOCK("+convert(src.op0())+");";
3036 }
3037 
3039  const codet &src,
3040  unsigned indent)
3041 {
3042  if(src.operands().size()!=1)
3043  {
3044  unsigned precedence;
3045  return convert_norep(src, precedence);
3046  }
3047 
3048  return indent_str(indent)+"UNLOCK("+convert(src.op0())+");";
3049 }
3050 
3052  const code_function_callt &src,
3053  unsigned indent)
3054 {
3055  if(src.operands().size()!=3)
3056  {
3057  unsigned precedence;
3058  return convert_norep(src, precedence);
3059  }
3060 
3061  std::string dest=indent_str(indent);
3062 
3063  if(src.lhs().is_not_nil())
3064  {
3065  unsigned p;
3066  std::string lhs_str=convert_with_precedence(src.lhs(), p);
3067 
3068  // TODO: ggf. Klammern je nach p
3069  dest+=lhs_str;
3070  dest+='=';
3071  }
3072 
3073  {
3074  unsigned p;
3075  std::string function_str=convert_with_precedence(src.function(), p);
3076  dest+=function_str;
3077  }
3078 
3079  dest+='(';
3080 
3081  const exprt::operandst &arguments=src.arguments();
3082 
3083  forall_expr(it, arguments)
3084  {
3085  unsigned p;
3086  std::string arg_str=convert_with_precedence(*it, p);
3087 
3088  if(it!=arguments.begin())
3089  dest+=", ";
3090  // TODO: ggf. Klammern je nach p
3091  dest+=arg_str;
3092  }
3093 
3094  dest+=");";
3095 
3096  return dest;
3097 }
3098 
3100  const codet &src,
3101  unsigned indent)
3102 {
3103  std::string dest=indent_str(indent)+"printf(";
3104 
3105  forall_operands(it, src)
3106  {
3107  unsigned p;
3108  std::string arg_str=convert_with_precedence(*it, p);
3109 
3110  if(it!=src.operands().begin())
3111  dest+=", ";
3112  // TODO: ggf. Klammern je nach p
3113  dest+=arg_str;
3114  }
3115 
3116  dest+=");";
3117 
3118  return dest;
3119 }
3120 
3122  const codet &src,
3123  unsigned indent)
3124 {
3125  std::string dest=indent_str(indent)+"FENCE(";
3126 
3127  irep_idt att[]=
3128  { ID_WRfence, ID_RRfence, ID_RWfence, ID_WWfence,
3129  ID_RRcumul, ID_RWcumul, ID_WWcumul, ID_WRcumul,
3130  irep_idt() };
3131 
3132  bool first=true;
3133 
3134  for(unsigned i=0; !att[i].empty(); i++)
3135  {
3136  if(src.get_bool(att[i]))
3137  {
3138  if(first)
3139  first=false;
3140  else
3141  dest+='+';
3142 
3143  dest+=id2string(att[i]);
3144  }
3145  }
3146 
3147  dest+=");";
3148  return dest;
3149 }
3150 
3152  const codet &src,
3153  unsigned indent)
3154 {
3155  std::string dest=indent_str(indent)+"INPUT(";
3156 
3157  forall_operands(it, src)
3158  {
3159  unsigned p;
3160  std::string arg_str=convert_with_precedence(*it, p);
3161 
3162  if(it!=src.operands().begin())
3163  dest+=", ";
3164  // TODO: ggf. Klammern je nach p
3165  dest+=arg_str;
3166  }
3167 
3168  dest+=");";
3169 
3170  return dest;
3171 }
3172 
3174  const codet &src,
3175  unsigned indent)
3176 {
3177  std::string dest=indent_str(indent)+"OUTPUT(";
3178 
3179  forall_operands(it, src)
3180  {
3181  unsigned p;
3182  std::string arg_str=convert_with_precedence(*it, p);
3183 
3184  if(it!=src.operands().begin())
3185  dest+=", ";
3186  dest+=arg_str;
3187  }
3188 
3189  dest+=");";
3190 
3191  return dest;
3192 }
3193 
3195  const codet &src,
3196  unsigned indent)
3197 {
3198  std::string dest=indent_str(indent)+"ARRAY_SET(";
3199 
3200  forall_operands(it, src)
3201  {
3202  unsigned p;
3203  std::string arg_str=convert_with_precedence(*it, p);
3204 
3205  if(it!=src.operands().begin())
3206  dest+=", ";
3207  // TODO: ggf. Klammern je nach p
3208  dest+=arg_str;
3209  }
3210 
3211  dest+=");";
3212 
3213  return dest;
3214 }
3215 
3217  const codet &src,
3218  unsigned indent)
3219 {
3220  std::string dest=indent_str(indent)+"ARRAY_COPY(";
3221 
3222  forall_operands(it, src)
3223  {
3224  unsigned p;
3225  std::string arg_str=convert_with_precedence(*it, p);
3226 
3227  if(it!=src.operands().begin())
3228  dest+=", ";
3229  // TODO: ggf. Klammern je nach p
3230  dest+=arg_str;
3231  }
3232 
3233  dest+=");";
3234 
3235  return dest;
3236 }
3237 
3239  const codet &src,
3240  unsigned indent)
3241 {
3242  std::string dest=indent_str(indent)+"ARRAY_REPLACE(";
3243 
3244  forall_operands(it, src)
3245  {
3246  unsigned p;
3247  std::string arg_str=convert_with_precedence(*it, p);
3248 
3249  if(it!=src.operands().begin())
3250  dest+=", ";
3251  dest+=arg_str;
3252  }
3253 
3254  dest+=");";
3255 
3256  return dest;
3257 }
3258 
3260  const codet &src,
3261  unsigned indent)
3262 {
3263  if(src.operands().size()!=1)
3264  {
3265  unsigned precedence;
3266  return convert_norep(src, precedence);
3267  }
3268 
3269  return indent_str(indent)+"assert("+convert(src.op0())+");";
3270 }
3271 
3273  const codet &src,
3274  unsigned indent)
3275 {
3276  if(src.operands().size()!=1)
3277  {
3278  unsigned precedence;
3279  return convert_norep(src, precedence);
3280  }
3281 
3282  return indent_str(indent) + CPROVER_PREFIX + "assume(" + convert(src.op0()) +
3283  ");";
3284 }
3285 
3287  const code_labelt &src,
3288  unsigned indent)
3289 {
3290  std::string labels_string;
3291 
3292  irep_idt label=src.get_label();
3293 
3294  labels_string+="\n";
3295  labels_string+=indent_str(indent);
3296  labels_string+=clean_identifier(label);
3297  labels_string+=":\n";
3298 
3299  std::string tmp=convert_code(src.code(), indent+2);
3300 
3301  return labels_string+tmp;
3302 }
3303 
3305  const code_switch_caset &src,
3306  unsigned indent)
3307 {
3308  std::string labels_string;
3309 
3310  if(src.is_default())
3311  {
3312  labels_string+="\n";
3313  labels_string+=indent_str(indent);
3314  labels_string+="default:\n";
3315  }
3316  else
3317  {
3318  labels_string+="\n";
3319  labels_string+=indent_str(indent);
3320  labels_string+="case ";
3321  labels_string+=convert(src.case_op());
3322  labels_string+=":\n";
3323  }
3324 
3325  unsigned next_indent=indent;
3326  if(src.code().get_statement()!=ID_block &&
3327  src.code().get_statement()!=ID_switch_case)
3328  next_indent+=2;
3329  std::string tmp=convert_code(src.code(), next_indent);
3330 
3331  return labels_string+tmp;
3332 }
3333 
3334 std::string expr2ct::convert_code(const codet &src)
3335 {
3336  return convert_code(src, 0);
3337 }
3338 
3339 std::string expr2ct::convert_Hoare(const exprt &src)
3340 {
3341  unsigned precedence;
3342 
3343  if(src.operands().size()!=2)
3344  return convert_norep(src, precedence);
3345 
3346  const exprt &assumption=src.op0();
3347  const exprt &assertion=src.op1();
3348  const codet &code=
3349  static_cast<const codet &>(src.find(ID_code));
3350 
3351  std::string dest="\n";
3352  dest+='{';
3353 
3354  if(!assumption.is_nil())
3355  {
3356  std::string assumption_str=convert(assumption);
3357  dest+=" assume(";
3358  dest+=assumption_str;
3359  dest+=");\n";
3360  }
3361  else
3362  dest+="\n";
3363 
3364  {
3365  std::string code_str=convert_code(code);
3366  dest+=code_str;
3367  }
3368 
3369  if(!assertion.is_nil())
3370  {
3371  std::string assertion_str=convert(assertion);
3372  dest+=" assert(";
3373  dest+=assertion_str;
3374  dest+=");\n";
3375  }
3376 
3377  dest+='}';
3378 
3379  return dest;
3380 }
3381 
3383  const exprt &src,
3384  unsigned precedence)
3385 {
3386  if(src.operands().size()!=2)
3387  return convert_norep(src, precedence);
3388 
3389  std::string dest=convert_with_precedence(src.op0(), precedence);
3390  dest+='[';
3391  dest+=convert_with_precedence(src.op1(), precedence);
3392  dest+=']';
3393 
3394  return dest;
3395 }
3396 
3398  const exprt &src,
3399  unsigned precedence)
3400 {
3401  if(src.operands().size()!=3)
3402  return convert_norep(src, precedence);
3403 
3404  std::string dest=convert_with_precedence(src.op0(), precedence);
3405  dest+='[';
3406  dest+=convert_with_precedence(src.op1(), precedence);
3407  dest+=", ";
3408  dest+=convert_with_precedence(src.op2(), precedence);
3409  dest+=']';
3410 
3411  return dest;
3412 }
3413 
3415  const exprt &src,
3416  unsigned &precedence)
3417 {
3418  if(src.has_operands())
3419  return convert_norep(src, precedence);
3420 
3421  std::string dest="sizeof(";
3422  dest+=convert(static_cast<const typet&>(src.find(ID_type_arg)));
3423  dest+=')';
3424 
3425  return dest;
3426 }
3427 
3429  const exprt &src,
3430  unsigned &precedence)
3431 {
3432  precedence=16;
3433 
3434  if(src.id()==ID_plus)
3435  return convert_multi_ary(src, "+", precedence=12, false);
3436 
3437  else if(src.id()==ID_minus)
3438  return convert_binary(src, "-", precedence=12, true);
3439 
3440  else if(src.id()==ID_unary_minus)
3441  return convert_unary(src, "-", precedence=15);
3442 
3443  else if(src.id()==ID_unary_plus)
3444  return convert_unary(src, "+", precedence=15);
3445 
3446  else if(src.id()==ID_floatbv_plus)
3447  return convert_function(src, "FLOAT+", precedence=16);
3448 
3449  else if(src.id()==ID_floatbv_minus)
3450  return convert_function(src, "FLOAT-", precedence=16);
3451 
3452  else if(src.id()==ID_floatbv_mult)
3453  return convert_function(src, "FLOAT*", precedence=16);
3454 
3455  else if(src.id()==ID_floatbv_div)
3456  return convert_function(src, "FLOAT/", precedence=16);
3457 
3458  else if(src.id()==ID_floatbv_rem)
3459  return convert_function(src, "FLOAT%", precedence=16);
3460 
3461  else if(src.id()==ID_floatbv_typecast)
3462  {
3463  precedence=16;
3464  std::string dest="FLOAT_TYPECAST(";
3465 
3466  unsigned p0;
3467  std::string tmp0=convert_with_precedence(src.op0(), p0);
3468 
3469  if(p0<=1)
3470  dest+='(';
3471  dest+=tmp0;
3472  if(p0<=1)
3473  dest+=')';
3474 
3475  const typet &to_type=ns.follow(src.type());
3476  dest+=", ";
3477  dest+=convert(to_type);
3478  dest+=", ";
3479 
3480  unsigned p1;
3481  std::string tmp1=convert_with_precedence(src.op1(), p1);
3482 
3483  if(p1<=1)
3484  dest+='(';
3485  dest+=tmp1;
3486  if(p1<=1)
3487  dest+=')';
3488 
3489  dest+=')';
3490  return dest;
3491  }
3492 
3493  else if(src.id()==ID_sign)
3494  {
3495  if(src.operands().size()==1 &&
3496  src.op0().type().id()==ID_floatbv)
3497  return convert_function(src, "signbit", precedence=16);
3498  else
3499  return convert_function(src, "SIGN", precedence=16);
3500  }
3501 
3502  else if(src.id()==ID_popcount)
3503  {
3505  return convert_function(src, "__popcnt", precedence=16);
3506  else
3507  return convert_function(src, "__builtin_popcount", precedence=16);
3508  }
3509 
3510  else if(src.id() == ID_r_ok)
3511  return convert_function(src, "R_OK", precedence = 16);
3512 
3513  else if(src.id() == ID_w_ok)
3514  return convert_function(src, "W_OK", precedence = 16);
3515 
3516  else if(src.id()==ID_invalid_pointer)
3517  return convert_function(src, "INVALID-POINTER", precedence=16);
3518 
3519  else if(src.id()==ID_good_pointer)
3520  return convert_function(src, "GOOD_POINTER", precedence=16);
3521 
3522  else if(src.id()==ID_object_size)
3523  return convert_function(src, "OBJECT_SIZE", precedence=16);
3524 
3525  else if(src.id()=="pointer_arithmetic")
3526  return convert_pointer_arithmetic(src, precedence=16);
3527 
3528  else if(src.id()=="pointer_difference")
3529  return convert_pointer_difference(src, precedence=16);
3530 
3531  else if(src.id() == ID_null_object)
3532  return "NULL-object";
3533 
3534  else if(src.id()==ID_integer_address ||
3535  src.id()==ID_integer_address_object ||
3536  src.id()==ID_stack_object ||
3537  src.id()==ID_static_object)
3538  {
3539  return id2string(src.id());
3540  }
3541 
3542  else if(src.id()==ID_infinity)
3543  return convert_function(src, "INFINITY", precedence=16);
3544 
3545  else if(src.id()=="builtin-function")
3546  return src.get_string(ID_identifier);
3547 
3548  else if(src.id()==ID_pointer_object)
3549  return convert_function(src, "POINTER_OBJECT", precedence=16);
3550 
3551  else if(src.id()=="get_must")
3552  return convert_function(src, CPROVER_PREFIX "get_must", precedence = 16);
3553 
3554  else if(src.id()=="get_may")
3555  return convert_function(src, CPROVER_PREFIX "get_may", precedence = 16);
3556 
3557  else if(src.id()=="object_value")
3558  return convert_function(src, "OBJECT_VALUE", precedence=16);
3559 
3560  else if(src.id()==ID_array_of)
3561  return convert_array_of(src, precedence=16);
3562 
3563  else if(src.id()==ID_pointer_offset)
3564  return convert_function(src, "POINTER_OFFSET", precedence=16);
3565 
3566  else if(src.id()=="pointer_base")
3567  return convert_function(src, "POINTER_BASE", precedence=16);
3568 
3569  else if(src.id()=="pointer_cons")
3570  return convert_function(src, "POINTER_CONS", precedence=16);
3571 
3572  else if(src.id()==ID_invalid_pointer)
3573  return convert_function(
3574  src, CPROVER_PREFIX "invalid_pointer", precedence = 16);
3575 
3576  else if(src.id()==ID_dynamic_object)
3577  return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
3578 
3579  else if(src.id()=="is_zero_string")
3580  return convert_function(src, "IS_ZERO_STRING", precedence=16);
3581 
3582  else if(src.id()=="zero_string")
3583  return convert_function(src, "ZERO_STRING", precedence=16);
3584 
3585  else if(src.id()=="zero_string_length")
3586  return convert_function(src, "ZERO_STRING_LENGTH", precedence=16);
3587 
3588  else if(src.id()=="buffer_size")
3589  return convert_function(src, "BUFFER_SIZE", precedence=16);
3590 
3591  else if(src.id()==ID_isnan)
3592  return convert_function(src, "isnan", precedence=16);
3593 
3594  else if(src.id()==ID_isfinite)
3595  return convert_function(src, "isfinite", precedence=16);
3596 
3597  else if(src.id()==ID_isinf)
3598  return convert_function(src, "isinf", precedence=16);
3599 
3600  else if(src.id()==ID_bswap)
3601  return convert_function(
3602  src,
3603  "__builtin_bswap" +
3605  precedence = 16);
3606 
3607  else if(src.id()==ID_isnormal)
3608  return convert_function(src, "isnormal", precedence=16);
3609 
3610  else if(src.id()==ID_builtin_offsetof)
3611  return convert_function(src, "builtin_offsetof", precedence=16);
3612 
3613  else if(src.id()==ID_gcc_builtin_va_arg)
3614  return convert_function(src, "gcc_builtin_va_arg", precedence=16);
3615 
3616  else if(src.id()==ID_alignof)
3617  // C uses "_Alignof", C++ uses "alignof"
3618  return convert_function(src, "alignof", precedence=16);
3619 
3620  else if(has_prefix(src.id_string(), "byte_extract"))
3621  return convert_byte_extract(src, precedence=16);
3622 
3623  else if(has_prefix(src.id_string(), "byte_update"))
3624  return convert_byte_update(src, precedence=16);
3625 
3626  else if(src.id()==ID_address_of)
3627  {
3628  if(src.operands().size()!=1)
3629  return convert_norep(src, precedence);
3630  else if(src.op0().id()==ID_label)
3631  return "&&"+src.op0().get_string(ID_identifier);
3632  else if(src.op0().id()==ID_index &&
3633  to_index_expr(src.op0()).index().is_zero())
3634  return convert(to_index_expr(src.op0()).array());
3635  else if(src.type().subtype().id()==ID_code)
3636  return convert_unary(src, "", precedence=15);
3637  else
3638  return convert_unary(src, "&", precedence=15);
3639  }
3640 
3641  else if(src.id()==ID_dereference)
3642  {
3643  if(src.operands().size()!=1)
3644  return convert_norep(src, precedence);
3645  else if(src.type().id()==ID_code)
3646  return convert_unary(src, "", precedence=15);
3647  else if(src.op0().id()==ID_plus &&
3648  src.op0().operands().size()==2 &&
3649  ns.follow(src.op0().op0().type()).id()==ID_pointer)
3650  {
3651  // Note that index[pointer] is legal C, but we avoid it nevertheless.
3652  return convert(index_exprt(src.op0().op0(), src.op0().op1()));
3653  }
3654  else
3655  return convert_unary(src, "*", precedence=15);
3656  }
3657 
3658  else if(src.id()==ID_index)
3659  return convert_index(src, precedence=16);
3660 
3661  else if(src.id()==ID_member)
3662  return convert_member(to_member_expr(src), precedence=16);
3663 
3664  else if(src.id()=="array-member-value")
3665  return convert_array_member_value(src, precedence=16);
3666 
3667  else if(src.id()=="struct-member-value")
3668  return convert_struct_member_value(src, precedence=16);
3669 
3670  else if(src.id()==ID_function_application)
3671  return
3673  to_function_application_expr(src), precedence);
3674 
3675  else if(src.id()==ID_side_effect)
3676  {
3677  const irep_idt &statement=src.get(ID_statement);
3678  if(statement==ID_preincrement)
3679  return convert_unary(src, "++", precedence=15);
3680  else if(statement==ID_predecrement)
3681  return convert_unary(src, "--", precedence=15);
3682  else if(statement==ID_postincrement)
3683  return convert_unary_post(src, "++", precedence=16);
3684  else if(statement==ID_postdecrement)
3685  return convert_unary_post(src, "--", precedence=16);
3686  else if(statement==ID_assign_plus)
3687  return convert_binary(src, "+=", precedence=2, true);
3688  else if(statement==ID_assign_minus)
3689  return convert_binary(src, "-=", precedence=2, true);
3690  else if(statement==ID_assign_mult)
3691  return convert_binary(src, "*=", precedence=2, true);
3692  else if(statement==ID_assign_div)
3693  return convert_binary(src, "/=", precedence=2, true);
3694  else if(statement==ID_assign_mod)
3695  return convert_binary(src, "%=", precedence=2, true);
3696  else if(statement==ID_assign_shl)
3697  return convert_binary(src, "<<=", precedence=2, true);
3698  else if(statement==ID_assign_shr)
3699  return convert_binary(src, ">>=", precedence=2, true);
3700  else if(statement==ID_assign_bitand)
3701  return convert_binary(src, "&=", precedence=2, true);
3702  else if(statement==ID_assign_bitxor)
3703  return convert_binary(src, "^=", precedence=2, true);
3704  else if(statement==ID_assign_bitor)
3705  return convert_binary(src, "|=", precedence=2, true);
3706  else if(statement==ID_assign)
3707  return convert_binary(src, "=", precedence=2, true);
3708  else if(statement==ID_function_call)
3709  return
3711  to_side_effect_expr_function_call(src), precedence);
3712  else if(statement == ID_allocate)
3713  return convert_allocate(src, precedence = 15);
3714  else if(statement==ID_printf)
3715  return convert_function(src, "printf", precedence=16);
3716  else if(statement==ID_nondet)
3717  return convert_nondet(src, precedence=16);
3718  else if(statement=="prob_coin")
3719  return convert_prob_coin(src, precedence=16);
3720  else if(statement=="prob_unif")
3721  return convert_prob_uniform(src, precedence=16);
3722  else if(statement==ID_statement_expression)
3723  return convert_statement_expression(src, precedence=15);
3724  else if(statement==ID_gcc_builtin_va_arg_next)
3725  return convert_function(src, "gcc_builtin_va_arg_next", precedence=16);
3726  else
3727  return convert_norep(src, precedence);
3728  }
3729 
3730  else if(src.id()==ID_literal)
3731  return convert_literal(src, precedence=16);
3732 
3733  else if(src.id()==ID_not)
3734  return convert_unary(src, "!", precedence=15);
3735 
3736  else if(src.id()==ID_bitnot)
3737  return convert_unary(src, "~", precedence=15);
3738 
3739  else if(src.id()==ID_mult)
3740  return convert_multi_ary(src, "*", precedence=13, false);
3741 
3742  else if(src.id()==ID_div)
3743  return convert_binary(src, "/", precedence=13, true);
3744 
3745  else if(src.id()==ID_mod)
3746  return convert_binary(src, "%", precedence=13, true);
3747 
3748  else if(src.id()==ID_shl)
3749  return convert_binary(src, "<<", precedence=11, true);
3750 
3751  else if(src.id()==ID_ashr || src.id()==ID_lshr)
3752  return convert_binary(src, ">>", precedence=11, true);
3753 
3754  else if(src.id()==ID_lt || src.id()==ID_gt ||
3755  src.id()==ID_le || src.id()==ID_ge)
3756  return convert_binary(src, src.id_string(), precedence=10, true);
3757 
3758  else if(src.id()==ID_notequal)
3759  return convert_binary(src, "!=", precedence=9, true);
3760 
3761  else if(src.id()==ID_equal)
3762  return convert_binary(src, "==", precedence=9, true);
3763 
3764  else if(src.id()==ID_ieee_float_equal)
3765  return convert_function(src, "IEEE_FLOAT_EQUAL", precedence=16);
3766 
3767  else if(src.id()==ID_width)
3768  return convert_function(src, "WIDTH", precedence=16);
3769 
3770  else if(src.id()==ID_concatenation)
3771  return convert_function(src, "CONCATENATION", precedence=16);
3772 
3773  else if(src.id()==ID_ieee_float_notequal)
3774  return convert_function(src, "IEEE_FLOAT_NOTEQUAL", precedence=16);
3775 
3776  else if(src.id()==ID_abs)
3777  return convert_function(src, "abs", precedence=16);
3778 
3779  else if(src.id()==ID_complex_real)
3780  return convert_function(src, "__real__", precedence=16);
3781 
3782  else if(src.id()==ID_complex_imag)
3783  return convert_function(src, "__imag__", precedence=16);
3784 
3785  else if(src.id()==ID_complex)
3786  return convert_complex(src, precedence=16);
3787 
3788  else if(src.id()==ID_bitand)
3789  return convert_multi_ary(src, "&", precedence=8, false);
3790 
3791  else if(src.id()==ID_bitxor)
3792  return convert_multi_ary(src, "^", precedence=7, false);
3793 
3794  else if(src.id()==ID_bitor)
3795  return convert_multi_ary(src, "|", precedence=6, false);
3796 
3797  else if(src.id()==ID_and)
3798  return convert_multi_ary(src, "&&", precedence=5, false);
3799 
3800  else if(src.id()==ID_or)
3801  return convert_multi_ary(src, "||", precedence=4, false);
3802 
3803  else if(src.id()==ID_xor)
3804  return convert_multi_ary(src, "!=", precedence = 9, false);
3805 
3806  else if(src.id()==ID_implies)
3807  return convert_binary(src, "==>", precedence=3, true);
3808 
3809  else if(src.id()==ID_if)
3810  return convert_trinary(src, "?", ":", precedence=3);
3811 
3812  else if(src.id()==ID_forall)
3813  return convert_quantifier(src, "forall", precedence=2);
3814 
3815  else if(src.id()==ID_exists)
3816  return convert_quantifier(src, "exists", precedence=2);
3817 
3818  else if(src.id()==ID_lambda)
3819  return convert_quantifier(src, "LAMBDA", precedence=2);
3820 
3821  else if(src.id()==ID_with)
3822  return convert_with(src, precedence=16);
3823 
3824  else if(src.id()==ID_update)
3825  return convert_update(src, precedence=16);
3826 
3827  else if(src.id()==ID_member_designator)
3828  return precedence=16, convert_member_designator(src);
3829 
3830  else if(src.id()==ID_index_designator)
3831  return precedence=16, convert_index_designator(src);
3832 
3833  else if(src.id()==ID_symbol)
3834  return convert_symbol(src, precedence);
3835 
3836  else if(src.id()==ID_next_symbol)
3837  return convert_symbol(src, precedence);
3838 
3839  else if(src.id()==ID_nondet_symbol)
3840  return convert_nondet_symbol(to_nondet_symbol_expr(src), precedence);
3841 
3842  else if(src.id()==ID_predicate_symbol)
3843  return convert_predicate_symbol(src, precedence);
3844 
3845  else if(src.id()==ID_predicate_next_symbol)
3846  return convert_predicate_next_symbol(src, precedence);
3847 
3848  else if(src.id()==ID_predicate_passive_symbol)
3849  return convert_predicate_passive_symbol(src, precedence);
3850 
3851  else if(src.id()=="quant_symbol")
3852  return convert_quantified_symbol(src, precedence);
3853 
3854  else if(src.id()==ID_nondet_bool)
3855  return convert_nondet_bool(src, precedence);
3856 
3857  else if(src.id()==ID_object_descriptor)
3858  return convert_object_descriptor(src, precedence);
3859 
3860  else if(src.id()=="Hoare")
3861  return convert_Hoare(src);
3862 
3863  else if(src.id()==ID_code)
3864  return convert_code(to_code(src));
3865 
3866  else if(src.id()==ID_constant)
3867  return convert_constant(to_constant_expr(src), precedence);
3868 
3869  else if(src.id()==ID_string_constant)
3870  return '"'+MetaString(src.get_string(ID_value))+'"';
3871 
3872  else if(src.id()==ID_struct)
3873  return convert_struct(src, precedence);
3874 
3875  else if(src.id()==ID_vector)
3876  return convert_vector(src, precedence);
3877 
3878  else if(src.id()==ID_union)
3879  return convert_union(src, precedence);
3880 
3881  else if(src.id()==ID_array)
3882  return convert_array(src, precedence);
3883 
3884  else if(src.id() == ID_array_list)
3885  return convert_array_list(src, precedence);
3886 
3887  else if(src.id()==ID_typecast)
3888  return convert_typecast(to_typecast_expr(src), precedence=14);
3889 
3890  else if(src.id()==ID_comma)
3891  return convert_comma(src, precedence=1);
3892 
3893  else if(src.id()==ID_ptr_object)
3894  return "PTR_OBJECT("+id2string(src.get(ID_identifier))+")";
3895 
3896  else if(src.id()==ID_cond)
3897  return convert_cond(src, precedence);
3898 
3899  else if(src.id()==ID_overflow_unary_minus ||
3900  src.id()==ID_overflow_minus ||
3901  src.id()==ID_overflow_mult ||
3902  src.id()==ID_overflow_plus)
3903  return convert_overflow(src, precedence);
3904 
3905  else if(src.id()==ID_unknown)
3906  return "*";
3907 
3908  else if(src.id()==ID_invalid)
3909  return "#";
3910 
3911  else if(src.id()==ID_extractbit)
3912  return convert_extractbit(src, precedence);
3913 
3914  else if(src.id()==ID_extractbits)
3915  return convert_extractbits(src, precedence);
3916 
3917  else if(src.id()==ID_initializer_list ||
3918  src.id()==ID_compound_literal)
3919  return convert_initializer_list(src, precedence=15);
3920 
3921  else if(src.id()==ID_designated_initializer)
3922  return convert_designated_initializer(src, precedence=15);
3923 
3924  else if(src.id()==ID_sizeof)
3925  return convert_sizeof(src, precedence);
3926 
3927  else if(src.id()==ID_let)
3928  return convert_let(to_let_expr(src), precedence=16);
3929 
3930  else if(src.id()==ID_type)
3931  return convert(src.type());
3932 
3933  // no C language expression for internal representation
3934  return convert_norep(src, precedence);
3935 }
3936 
3937 std::string expr2ct::convert(const exprt &src)
3938 {
3939  unsigned precedence;
3940  return convert_with_precedence(src, precedence);
3941 }
3942 
3949  const typet &src,
3950  const std::string &identifier)
3951 {
3952  return convert_rec(src, c_qualifierst(), identifier);
3953 }
3954 
3955 std::string expr2c(
3956  const exprt &expr,
3957  const namespacet &ns,
3958  const expr2c_configurationt &configuration)
3959 {
3960  std::string code;
3961  expr2ct expr2c(ns, configuration);
3962  expr2c.get_shorthands(expr);
3963  return expr2c.convert(expr);
3964 }
3965 
3966 std::string expr2c(const exprt &expr, const namespacet &ns)
3967 {
3969 }
3970 
3971 std::string type2c(
3972  const typet &type,
3973  const namespacet &ns,
3974  const expr2c_configurationt &configuration)
3975 {
3976  expr2ct expr2c(ns, configuration);
3977  // expr2c.get_shorthands(expr);
3978  return expr2c.convert(type);
3979 }
3980 
3981 std::string type2c(const typet &type, const namespacet &ns)
3982 {
3984 }
3985 
3986 std::string type2c(
3987  const typet &type,
3988  const std::string &identifier,
3989  const namespacet &ns,
3990  const expr2c_configurationt &configuration)
3991 {
3992  expr2ct expr2c(ns, configuration);
3993  return expr2c.convert_with_identifier(type, identifier);
3994 }
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1225
const irep_idt & get_statement() const
Definition: std_code.h:56
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1775
The type of an expression, extends irept.
Definition: type.h:27
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3272
const codet & then_case() const
Definition: std_code.h:652
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:188
struct configt::ansi_ct ansi_c
Semantic type conversion.
Definition: std_expr.h:2277
BigInt mp_integer
Definition: mp_arith.h:22
std::string convert_complex(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1311
std::string true_string
This is the string that will be printed for the true boolean expression.
Definition: expr2c.h:34
std::string to_ansi_c_string() const
Definition: fixedbv.h:62
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
virtual std::string convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
To generate C-like string for defining the given struct.
Definition: expr2c.cpp:675
const exprt & init() const
Definition: std_code.h:917
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:109
Application of (mathematical) function.
Definition: std_expr.h:4481
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2866
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1116
Symbol table entry.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1263
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:20
const exprt & cond() const
Definition: std_code.h:783
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
std::string convert_code_continue(const codet &src, unsigned indent)
Definition: expr2c.cpp:2721
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3971
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3121
const exprt & op() const
Definition: std_expr.h:371
const exprt & cond() const
Definition: std_code.h:642
std::string expr2string() const
Definition: lispexpr.cpp:15
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
std::string convert_Hoare(const exprt &src)
Definition: expr2c.cpp:3339
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const codet & body() const
Definition: std_code.h:947
bool has_ellipsis() const
Definition: std_types.h:849
codet & code()
Definition: std_code.h:1361
const codet & body() const
Definition: std_code.h:855
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2163
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
std::size_t single_width
Definition: config.h:37
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1427
const irep_idt & get_function() const
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
#define forall_expr(it, expr)
Definition: expr.h:31
code_operandst & statements()
Definition: std_code.h:159
std::vector< componentt > componentst
Definition: std_types.h:203
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition: expr2c.cpp:3304
const irep_idt & get_value() const
Definition: std_expr.h:4403
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
literalt pos(literalt a)
Definition: literal.h:193
std::vector< parametert > parameterst
Definition: std_types.h:754
argumentst & arguments()
Definition: std_expr.h:4506
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2427
exprt build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:557
const componentst & components() const
Definition: std_types.h:205
ANSI-C Misc Utilities.
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition: expr2c.cpp:2828
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3334
bool NULL_is_zero
Definition: config.h:87
std::size_t get_component_number() const
Definition: std_expr.h:3925
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
const memberst & members() const
Definition: std_types.h:674
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1362
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3038
typet & type()
Return the type of the expression.
Definition: expr.h:68
unsignedbv_typet size_type()
Definition: c_types.cpp:58
std::size_t double_width
Definition: config.h:38
const irep_idt & get_flavor() const
Definition: std_code.h:1471
Symbol table entry.
Definition: symbol.h:27
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1674
A constant literal expression.
Definition: std_expr.h:4384
Structure type, corresponds to C style structs.
Definition: std_types.h:276
std::string convert_code_break(const codet &src, unsigned indent)
Definition: expr2c.cpp:2667
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2732
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
configt config
Definition: config.cpp:24
std::size_t char_width
Definition: config.h:33
std::string convert_code_return(const codet &src, unsigned indent)
Definition: expr2c.cpp:2633
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1732
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:183
std::string convert_with_identifier(const typet &src, const std::string &identifier)
Build a declaration string, which requires converting both a type and putting an identifier in the sy...
Definition: expr2c.cpp:3948
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2c.cpp:3051
std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence)
Definition: expr2c.cpp:1716
bool is_static_lifetime
Definition: symbol.h:65
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:66
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4683
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3414
const expr2c_configurationt & configuration
Definition: expr2c_class.h:47
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3099
const exprt & case_op() const
Definition: std_code.h:1351
unsigned sizeof_nesting
Definition: expr2c_class.h:82
Extract member of struct or union.
Definition: std_expr.h:3890
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program...
Definition: expr2c.h:55
exprt & where()
Definition: std_expr.h:4666
std::string convert_binary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1061
std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1740
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1787
std::string convert_unary(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1165
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2027
const irep_idt & id() const
Definition: irep.h:259
std::string convert_literal(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1246
std::size_t long_long_int_width
Definition: config.h:35
std::string convert_code_assign(const code_assignt &src, unsigned indent)
Definition: expr2c.cpp:3014
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3286
argumentst & arguments()
Definition: std_code.h:1109
std::string convert_byte_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1397
A reference into the symbol table.
Definition: std_types.h:62
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1756
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3151
flavourt mode
Definition: config.h:115
const irep_idt & get_identifier() const
Definition: std_expr.h:293
bool is_exported
Definition: symbol.h:61
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:79
virtual std::unique_ptr< qualifierst > clone() const =0
bool is_parameter
Definition: symbol.h:66
const exprt & cond() const
Definition: std_code.h:927
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1236
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
codet & code()
Definition: std_code.h:1289
std::size_t get_fraction_bits() const
Definition: std_types.h:1344
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1557
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:876
The vector type.
Definition: std_types.h:1755
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:814
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3194
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1567
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1510
std::string convert_trinary(const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
Definition: expr2c.cpp:823
std::string convert_code_asm(const code_asmt &src, unsigned indent)
Definition: expr2c.cpp:2463
exprt & op1()
Definition: expr.h:87
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: std_expr.h:4523
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const exprt & size() const
Definition: std_types.h:1765
virtual void read(const typet &src) override
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2321
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2777
codet representation of a label for branch targets.
Definition: std_code.h:1256
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1238
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3025
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
std::size_t int_width
Definition: config.h:30
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
#define forall_operands(it, expr)
Definition: expr.h:20
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2287
std::string convert_with(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:895
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
const namespacet & ns
Definition: expr2c_class.h:46
codet representing a while statement.
Definition: std_code.h:767
size_t size() const
Definition: dstring.h:91
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1253
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1382
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
void irep2lisp(const irept &src, lispexprt &dest)
Definition: lispirep.cpp:43
std::unordered_map< irep_idt, irep_idt > shorthands
Definition: expr2c_class.h:80
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
std::string convert_extractbits(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3397
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
virtual std::string as_string() const override
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3382
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
Definition: expr2c.cpp:2397
bool include_struct_padding_components
When printing struct_typet or struct_exprt, include the artificial padding components introduced to k...
Definition: expr2c.h:24
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool char_is_unsigned
Definition: config.h:43
std::size_t get_width() const
Definition: std_types.h:1117
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2116
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:258
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
const irep_idt & get_pretty_name() const
Definition: std_types.h:162
symbol_exprt & function()
Definition: std_expr.h:4496
std::vector< exprt > operandst
Definition: expr.h:57
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1724
Pointer Logic.
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1215
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1663
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3259
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1449
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1643
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
bool is_extern
Definition: symbol.h:66
std::string convert_byte_extract(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1372
bool print_struct_body_in_type
When printing a struct_typet, should the components of the struct be printed inline.
Definition: expr2c.h:28
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1547
floatbv_typet long_double_type()
Definition: c_types.cpp:201
floatbv_typet float_type()
Definition: c_types.cpp:185
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
bool include_array_size
When printing array_typet, should the size of the array be printed.
Definition: expr2c.h:31
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition: expr2c.cpp:2567
exprt & value()
Definition: std_expr.h:4656
Expression to hold a nondeterministic choice.
Definition: std_expr.h:277
Base type for structs and unions.
Definition: std_types.h:114
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1748
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3216
exprt & function()
Definition: std_code.h:1099
bool is_default() const
Definition: std_code.h:1341
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
std::string convert_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:983
The union type.
Definition: std_types.h:425
std::string convert_cond(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1027
floatbv_typet double_type()
Definition: c_types.cpp:193
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
std::string convert_code_for(const code_fort &src, unsigned indent)
Definition: expr2c.cpp:2791
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3955
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
codet representation of a do while statement.
Definition: std_code.h:829
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
const source_locationt & source_location() const
Definition: expr.h:228
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3428
codet representation of an inline assembler statement.
Definition: std_code.h:1459
const exprt & iter() const
Definition: std_code.h:937
irep_idt get_component_name() const
Definition: std_expr.h:3915
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2851
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3238
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
bool is_file_local
Definition: symbol.h:66
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1473
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
exprt::operandst & arguments()
Definition: std_code.h:1754
const std::string & id_string() const
Definition: irep.h:262
std::string false_string
This is the string that will be printed for the false boolean expression.
Definition: expr2c.h:37
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
A codet representing sequential composition of program statements.
Definition: std_code.h:150
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1653
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
std::string convert_array(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2184
const irep_idt & get_label() const
Definition: std_code.h:1279
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1188
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:968
codet representation of an if-then-else statement.
Definition: std_code.h:614
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
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2349
exprt & op2()
Definition: expr.h:90
const char * c_str() const
Definition: dstring.h:86
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1326
symbol_exprt & symbol()
Definition: std_expr.h:4646
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:697
std::string convert_code_goto(const codet &src, unsigned indent)
Definition: expr2c.cpp:2655
dstringt irep_idt
Definition: irep.h:32
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
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
const irep_idt & get_comment() const
codet representation of a for statement.
Definition: std_code.h:893
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1310
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1287
A let expression.
Definition: std_expr.h:4635
const typet & subtype() const
Definition: type.h:38
irep_idt get_tag() const
Definition: std_types.h:226
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition: expr2c.cpp:2541
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3173
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1763
std::string to_ansi_c_string() const
Definition: ieee_float.h:269
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:305
static std::string clean_identifier(const irep_idt &id)
Definition: expr2c.cpp:84
bool get_inlined() const
Definition: std_types.h:903
operandst & operands()
Definition: expr.h:78
std::size_t long_int_width
Definition: config.h:31
const exprt & cond() const
Definition: std_code.h:845
const codet & else_case() const
Definition: std_code.h:662
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:688
std::vector< c_enum_membert > memberst
Definition: std_types.h:672
bool empty() const
Definition: dstring.h:75
std::string convert_quantifier(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:873
std::string convert_let(const let_exprt &, unsigned precedence)
Definition: expr2c.cpp:963
const codet & body() const
Definition: std_code.h:793
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition: expr2c.cpp:2019
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
void find_symbols(const exprt &src, find_symbols_sett &dest)
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1490
bitvector_typet char_type()
Definition: c_types.cpp:114
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:711
const typet & return_type() const
Definition: std_types.h:883
std::string convert_code_switch(const codet &src, unsigned indent)
Definition: expr2c.cpp:2678
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:789
A codet representing an assignment in the program.
Definition: std_code.h:256
std::size_t short_int_width
Definition: config.h:34
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2458
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2367
virtual std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
To generate a C-like type declaration of an array.
Definition: expr2c.cpp:752
std::size_t long_double_width
Definition: config.h:39
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
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition: expr2c.cpp:2596
Array index operator.
Definition: std_expr.h:1595
exprt & op3()
Definition: expr.h:93
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition: expr2c.h:59