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