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 
1167 std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
1168 {
1169  if(src.operands().size() != 2)
1170  return convert_norep(src, precedence);
1171 
1172  unsigned p0;
1173  std::string op0 = convert_with_precedence(src.op0(), p0);
1174 
1175  unsigned p1;
1176  std::string op1 = convert_with_precedence(src.op1(), p1);
1177 
1178  std::string dest = "ALLOCATE";
1179  dest += '(';
1180 
1181  if(src.type().id()==ID_pointer &&
1182  src.type().subtype().id()!=ID_empty)
1183  {
1184  dest+=convert(src.type().subtype());
1185  dest+=", ";
1186  }
1187 
1188  dest += op0 + ", " + op1;
1189  dest += ')';
1190 
1191  return dest;
1192 }
1193 
1195  const exprt &src,
1196  unsigned &precedence)
1197 {
1198  if(!src.operands().empty())
1199  return convert_norep(src, precedence);
1200 
1201  return "NONDET("+convert(src.type())+")";
1202 }
1203 
1205  const exprt &src,
1206  unsigned &precedence)
1207 {
1208  if(src.operands().size()!=1 ||
1209  to_code(src.op0()).get_statement()!=ID_block)
1210  return convert_norep(src, precedence);
1211 
1212  return "("+convert_code(to_code_block(to_code(src.op0())), 0)+")";
1213 }
1214 
1216  const exprt &src,
1217  unsigned &precedence)
1218 {
1219  if(src.operands().size()==1)
1220  return "COIN("+convert(src.op0())+")";
1221  else
1222  return convert_norep(src, precedence);
1223 }
1224 
1226  const exprt &src,
1227  unsigned &precedence)
1228 {
1229  return "L("+src.get_string(ID_literal)+")";
1230 }
1231 
1233  const exprt &src,
1234  unsigned &precedence)
1235 {
1236  if(src.operands().size()==1)
1237  return "PROB_UNIFORM("+convert(src.type())+","+convert(src.op0())+")";
1238  else
1239  return convert_norep(src, precedence);
1240 }
1241 
1243  const exprt &src,
1244  const std::string &name,
1245  unsigned precedence)
1246 {
1247  std::string dest=name;
1248  dest+='(';
1249 
1250  forall_operands(it, src)
1251  {
1252  unsigned p;
1253  std::string op=convert_with_precedence(*it, p);
1254 
1255  if(it!=src.operands().begin())
1256  dest+=", ";
1257 
1258  dest+=op;
1259  }
1260 
1261  dest+=')';
1262 
1263  return dest;
1264 }
1265 
1267  const exprt &src,
1268  unsigned precedence)
1269 {
1270  if(src.operands().size()!=2)
1271  return convert_norep(src, precedence);
1272 
1273  unsigned p0;
1274  std::string op0=convert_with_precedence(src.op0(), p0);
1275  if(*op0.rbegin()==';')
1276  op0.resize(op0.size()-1);
1277 
1278  unsigned p1;
1279  std::string op1=convert_with_precedence(src.op1(), p1);
1280  if(*op1.rbegin()==';')
1281  op1.resize(op1.size()-1);
1282 
1283  std::string dest=op0;
1284  dest+=", ";
1285  dest+=op1;
1286 
1287  return dest;
1288 }
1289 
1291  const exprt &src,
1292  unsigned precedence)
1293 {
1294  if(src.operands().size()==2 &&
1295  src.op0().is_zero() &&
1296  src.op1().id()==ID_constant)
1297  {
1298  // This is believed to be gcc only; check if this is sensible
1299  // in MSC mode.
1300  return convert_with_precedence(src.op1(), precedence)+"i";
1301  }
1302 
1303  // ISO C11 offers:
1304  // double complex CMPLX(double x, double y);
1305  // float complex CMPLXF(float x, float y);
1306  // long double complex CMPLXL(long double x, long double y);
1307 
1308  const typet &subtype=
1309  ns.follow(ns.follow(src.type()).subtype());
1310 
1311  std::string name;
1312 
1313  if(subtype==double_type())
1314  name="CMPLX";
1315  else if(subtype==float_type())
1316  name="CMPLXF";
1317  else if(subtype==long_double_type())
1318  name="CMPLXL";
1319  else
1320  name="CMPLX"; // default, possibly wrong
1321 
1322  std::string dest=name;
1323  dest+='(';
1324 
1325  forall_operands(it, src)
1326  {
1327  unsigned p;
1328  std::string op=convert_with_precedence(*it, p);
1329 
1330  if(it!=src.operands().begin())
1331  dest+=", ";
1332 
1333  dest+=op;
1334  }
1335 
1336  dest+=')';
1337 
1338  return dest;
1339 }
1340 
1342  const exprt &src,
1343  unsigned precedence)
1344 {
1345  if(src.operands().size()!=1)
1346  return convert_norep(src, precedence);
1347 
1348  return "ARRAY_OF("+convert(src.op0())+')';
1349 }
1350 
1352  const exprt &src,
1353  unsigned precedence)
1354 {
1355  if(src.operands().size()!=2)
1356  return convert_norep(src, precedence);
1357 
1358  unsigned p0;
1359  std::string op0=convert_with_precedence(src.op0(), p0);
1360 
1361  unsigned p1;
1362  std::string op1=convert_with_precedence(src.op1(), p1);
1363 
1364  std::string dest=src.id_string();
1365  dest+='(';
1366  dest+=op0;
1367  dest+=", ";
1368  dest+=op1;
1369  dest+=", ";
1370  dest+=convert(src.type());
1371  dest+=')';
1372 
1373  return dest;
1374 }
1375 
1377  const exprt &src,
1378  unsigned precedence)
1379 {
1380  if(src.operands().size()!=3)
1381  return convert_norep(src, precedence);
1382 
1383  unsigned p0;
1384  std::string op0=convert_with_precedence(src.op0(), p0);
1385 
1386  unsigned p1;
1387  std::string op1=convert_with_precedence(src.op1(), p1);
1388 
1389  unsigned p2;
1390  std::string op2=convert_with_precedence(src.op2(), p2);
1391 
1392  std::string dest=src.id_string();
1393  dest+='(';
1394  dest+=op0;
1395  dest+=", ";
1396  dest+=op1;
1397  dest+=", ";
1398  dest+=op2;
1399  dest+=", ";
1400  dest+=convert(src.op2().type());
1401  dest+=')';
1402 
1403  return dest;
1404 }
1405 
1407  const exprt &src,
1408  const std::string &symbol,
1409  unsigned precedence)
1410 {
1411  if(src.operands().size()!=1)
1412  return convert_norep(src, precedence);
1413 
1414  unsigned p;
1415  std::string op=convert_with_precedence(src.op0(), p);
1416 
1417  std::string dest;
1418  if(precedence>p)
1419  dest+='(';
1420  dest+=op;
1421  if(precedence>p)
1422  dest+=')';
1423  dest+=symbol;
1424 
1425  return dest;
1426 }
1427 
1429  const exprt &src,
1430  unsigned precedence)
1431 {
1432  if(src.operands().size()!=2)
1433  return convert_norep(src, precedence);
1434 
1435  unsigned p;
1436  std::string op=convert_with_precedence(src.op0(), p);
1437 
1438  std::string dest;
1439  if(precedence>p)
1440  dest+='(';
1441  dest+=op;
1442  if(precedence>p)
1443  dest+=')';
1444 
1445  dest+='[';
1446  dest+=convert(src.op1());
1447  dest+=']';
1448 
1449  return dest;
1450 }
1451 
1453  const exprt &src, unsigned &precedence)
1454 {
1455  if(src.operands().size()!=2)
1456  return convert_norep(src, precedence);
1457 
1458  std::string dest="POINTER_ARITHMETIC(";
1459 
1460  unsigned p;
1461  std::string op;
1462 
1463  op=convert(src.op0().type());
1464  dest+=op;
1465 
1466  dest+=", ";
1467 
1468  op=convert_with_precedence(src.op0(), p);
1469  if(precedence>p)
1470  dest+='(';
1471  dest+=op;
1472  if(precedence>p)
1473  dest+=')';
1474 
1475  dest+=", ";
1476 
1477  op=convert_with_precedence(src.op1(), p);
1478  if(precedence>p)
1479  dest+='(';
1480  dest+=op;
1481  if(precedence>p)
1482  dest+=')';
1483 
1484  dest+=')';
1485 
1486  return dest;
1487 }
1488 
1490  const exprt &src, unsigned &precedence)
1491 {
1492  if(src.operands().size()!=2)
1493  return convert_norep(src, precedence);
1494 
1495  std::string dest="POINTER_DIFFERENCE(";
1496 
1497  unsigned p;
1498  std::string op;
1499 
1500  op=convert(src.op0().type());
1501  dest+=op;
1502 
1503  dest+=", ";
1504 
1505  op=convert_with_precedence(src.op0(), p);
1506  if(precedence>p)
1507  dest+='(';
1508  dest+=op;
1509  if(precedence>p)
1510  dest+=')';
1511 
1512  dest+=", ";
1513 
1514  op=convert_with_precedence(src.op1(), p);
1515  if(precedence>p)
1516  dest+='(';
1517  dest+=op;
1518  if(precedence>p)
1519  dest+=')';
1520 
1521  dest+=')';
1522 
1523  return dest;
1524 }
1525 
1527 {
1528  unsigned precedence;
1529 
1530  if(!src.operands().empty())
1531  return convert_norep(src, precedence);
1532 
1533  return "."+src.get_string(ID_component_name);
1534 }
1535 
1537 {
1538  unsigned precedence;
1539 
1540  if(src.operands().size()!=1)
1541  return convert_norep(src, precedence);
1542 
1543  return "["+convert(src.op0())+"]";
1544 }
1545 
1547  const member_exprt &src,
1548  unsigned precedence)
1549 {
1550  if(src.operands().size()!=1)
1551  return convert_norep(src, precedence);
1552 
1553  unsigned p;
1554  std::string dest;
1555 
1556  if(src.op0().id()==ID_dereference &&
1557  src.operands().size()==1)
1558  {
1559  std::string op=convert_with_precedence(src.op0().op0(), p);
1560 
1561  if(precedence>p || src.op0().op0().id()==ID_typecast)
1562  dest+='(';
1563  dest+=op;
1564  if(precedence>p || src.op0().op0().id()==ID_typecast)
1565  dest+=')';
1566 
1567  dest+="->";
1568  }
1569  else
1570  {
1571  std::string op=convert_with_precedence(src.op0(), p);
1572 
1573  if(precedence>p || src.op0().id()==ID_typecast)
1574  dest+='(';
1575  dest+=op;
1576  if(precedence>p || src.op0().id()==ID_typecast)
1577  dest+=')';
1578 
1579  dest+='.';
1580  }
1581 
1582  const typet &full_type=ns.follow(src.op0().type());
1583 
1584  if(full_type.id()!=ID_struct &&
1585  full_type.id()!=ID_union)
1586  return convert_norep(src, precedence);
1587 
1588  const struct_union_typet &struct_union_type=
1589  to_struct_union_type(full_type);
1590 
1591  irep_idt component_name=src.get_component_name();
1592 
1593  if(component_name!="")
1594  {
1595  const exprt comp_expr=
1596  struct_union_type.get_component(component_name);
1597 
1598  if(comp_expr.is_nil())
1599  return convert_norep(src, precedence);
1600 
1601  if(!comp_expr.get(ID_pretty_name).empty())
1602  dest+=comp_expr.get_string(ID_pretty_name);
1603  else
1604  dest+=id2string(component_name);
1605 
1606  return dest;
1607  }
1608 
1609  std::size_t n=src.get_component_number();
1610 
1611  if(n>=struct_union_type.components().size())
1612  return convert_norep(src, precedence);
1613 
1614  const exprt comp_expr=
1615  struct_union_type.components()[n];
1616 
1617  dest+=comp_expr.get_string(ID_pretty_name);
1618 
1619  return dest;
1620 }
1621 
1623  const exprt &src,
1624  unsigned precedence)
1625 {
1626  if(src.operands().size()!=1)
1627  return convert_norep(src, precedence);
1628 
1629  return "[]="+convert(src.op0());
1630 }
1631 
1633  const exprt &src,
1634  unsigned precedence)
1635 {
1636  if(src.operands().size()!=1)
1637  return convert_norep(src, precedence);
1638 
1639  return "."+src.get_string(ID_name)+"="+convert(src.op0());
1640 }
1641 
1643  const exprt &src,
1644  unsigned &precedence)
1645 {
1646  lispexprt lisp;
1647  irep2lisp(src, lisp);
1648  std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
1649  precedence=16;
1650  return dest;
1651 }
1652 
1654  const exprt &src,
1655  unsigned &precedence)
1656 {
1657  const irep_idt &id=src.get(ID_identifier);
1658  std::string dest;
1659 
1660  if(src.operands().size()==1 &&
1661  src.op0().id()==ID_predicate_passive_symbol)
1662  dest=src.op0().get_string(ID_identifier);
1663  else
1664  {
1665  std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1666  shorthands.find(id);
1667  // we might be called from conversion of a type
1668  if(entry==shorthands.end())
1669  {
1670  get_shorthands(src);
1671 
1672  entry=shorthands.find(id);
1673  assert(entry!=shorthands.end());
1674  }
1675 
1676  dest=id2string(entry->second);
1677 
1678  #if 0
1679  if(has_prefix(id2string(id), "symex_dynamic::dynamic_object"))
1680  {
1681  if(sizeof_nesting++ == 0)
1682  dest+=" /*"+convert(src.type());
1683  if(--sizeof_nesting == 0)
1684  dest+="*/";
1685  }
1686  #endif
1687  }
1688 
1689  if(src.id()==ID_next_symbol)
1690  dest="NEXT("+dest+")";
1691 
1692  return dest;
1693 }
1694 
1696  const nondet_symbol_exprt &src,
1697  unsigned &precedence)
1698 {
1699  const irep_idt id=src.get_identifier();
1700  return "nondet_symbol("+id2string(id)+")";
1701 }
1702 
1704  const exprt &src,
1705  unsigned &precedence)
1706 {
1707  const std::string &id=src.get_string(ID_identifier);
1708  return "ps("+id+")";
1709 }
1710 
1712  const exprt &src,
1713  unsigned &precedence)
1714 {
1715  const std::string &id=src.get_string(ID_identifier);
1716  return "pns("+id+")";
1717 }
1718 
1720  const exprt &src,
1721  unsigned &precedence)
1722 {
1723  const std::string &id=src.get_string(ID_identifier);
1724  return "pps("+id+")";
1725 }
1726 
1728  const exprt &src,
1729  unsigned &precedence)
1730 {
1731  const std::string &id=src.get_string(ID_identifier);
1732  return id;
1733 }
1734 
1736  const exprt &src,
1737  unsigned &precedence)
1738 {
1739  return "nondet_bool()";
1740 }
1741 
1743  const exprt &src,
1744  unsigned &precedence)
1745 {
1746  if(src.operands().size()!=2)
1747  return convert_norep(src, precedence);
1748 
1749  std::string result="<";
1750 
1751  result+=convert(src.op0());
1752  result+=", ";
1753  result+=convert(src.op1());
1754  result+=", ";
1755 
1756  if(src.type().is_nil())
1757  result+='?';
1758  else
1759  result+=convert(src.type());
1760 
1761  result+='>';
1762 
1763  return result;
1764 }
1765 
1767  const constant_exprt &src,
1768  unsigned &precedence)
1769 {
1770  const irep_idt &base=src.get(ID_C_base);
1771  const typet &type=ns.follow(src.type());
1772  const irep_idt value=src.get_value();
1773  std::string dest;
1774 
1775  if(type.id()==ID_integer ||
1776  type.id()==ID_natural ||
1777  type.id()==ID_rational)
1778  {
1779  dest=id2string(value);
1780  }
1781  else if(type.id()==ID_c_enum ||
1782  type.id()==ID_c_enum_tag)
1783  {
1784  typet c_enum_type=
1785  type.id()==ID_c_enum?to_c_enum_type(type):
1787 
1788  if(c_enum_type.id()!=ID_c_enum)
1789  return convert_norep(src, precedence);
1790 
1791  bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
1792 
1793  mp_integer int_value=binary2integer(id2string(value), is_signed);
1794  mp_integer i=0;
1795 
1796  irep_idt int_value_string=integer2string(int_value);
1797 
1798  const c_enum_typet::memberst &members=
1799  to_c_enum_type(c_enum_type).members();
1800 
1801  for(c_enum_typet::memberst::const_iterator
1802  it=members.begin();
1803  it!=members.end();
1804  it++)
1805  {
1806  if(it->get_value()==int_value_string)
1807  return "/*enum*/"+id2string(it->get_base_name());
1808  }
1809 
1810  // failed...
1811  return "/*enum*/"+integer2string(int_value);
1812  }
1813  else if(type.id()==ID_rational)
1814  return convert_norep(src, precedence);
1815  else if(type.id()==ID_bv)
1816  {
1817  // not C
1818  dest=id2string(value);
1819  }
1820  else if(type.id()==ID_bool)
1821  {
1822  dest=convert_constant_bool(src.is_true());
1823  }
1824  else if(type.id()==ID_unsignedbv ||
1825  type.id()==ID_signedbv ||
1826  type.id()==ID_c_bit_field ||
1827  type.id()==ID_c_bool)
1828  {
1829  mp_integer int_value=
1830  binary2integer(id2string(value), type.id()==ID_signedbv);
1831 
1832  const irep_idt &c_type=
1833  type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
1834  type.get(ID_C_c_type);
1835 
1836  if(type.id()==ID_c_bool)
1837  {
1838  dest=convert_constant_bool(int_value!=0);
1839  }
1840  else if(type==char_type() &&
1841  type!=signed_int_type() &&
1842  type!=unsigned_int_type())
1843  {
1844  if(int_value=='\n')
1845  dest+="'\\n'";
1846  else if(int_value=='\r')
1847  dest+="'\\r'";
1848  else if(int_value=='\t')
1849  dest+="'\\t'";
1850  else if(int_value=='\'')
1851  dest+="'\\''";
1852  else if(int_value=='\\')
1853  dest+="'\\\\'";
1854  else if(int_value>=' ' && int_value<126)
1855  {
1856  dest+='\'';
1857  dest+=static_cast<char>(integer2ulong(int_value));
1858  dest+='\'';
1859  }
1860  else
1861  dest=integer2string(int_value);
1862  }
1863  else
1864  {
1865  if(base=="16")
1866  dest="0x"+integer2string(int_value, 16);
1867  else if(base=="8")
1868  dest="0"+integer2string(int_value, 8);
1869  else if(base=="2")
1870  dest="0b"+integer2string(int_value, 2);
1871  else
1872  dest=integer2string(int_value);
1873 
1874  if(c_type==ID_unsigned_int)
1875  dest+='u';
1876  else if(c_type==ID_unsigned_long_int)
1877  dest+="ul";
1878  else if(c_type==ID_signed_long_int)
1879  dest+='l';
1880  else if(c_type==ID_unsigned_long_long_int)
1881  dest+="ull";
1882  else if(c_type==ID_signed_long_long_int)
1883  dest+="ll";
1884 
1885  if(src.find(ID_C_c_sizeof_type).is_not_nil() &&
1886  sizeof_nesting==0)
1887  {
1888  const exprt sizeof_expr = build_sizeof_expr(to_constant_expr(src), ns);
1889 
1890  if(sizeof_expr.is_not_nil())
1891  {
1892  ++sizeof_nesting;
1893  dest=convert(sizeof_expr)+" /*"+dest+"*/ ";
1894  --sizeof_nesting;
1895  }
1896  }
1897  }
1898  }
1899  else if(type.id()==ID_floatbv)
1900  {
1902 
1903  if(dest!="" && isdigit(dest[dest.size()-1]))
1904  {
1905  if(dest.find('.')==std::string::npos)
1906  dest+=".0";
1907 
1908  // ANSI-C: double is default; float/long-double require annotation
1909  if(src.type()==float_type())
1910  dest+='f';
1911  else if(src.type()==long_double_type() &&
1913  dest+='l';
1914  }
1915  else if(dest.size()==4 &&
1916  (dest[0]=='+' || dest[0]=='-'))
1917  {
1918  if(dest=="+inf")
1919  dest="+INFINITY";
1920  else if(dest=="-inf")
1921  dest="-INFINITY";
1922  else if(dest=="+NaN")
1923  dest="+NAN";
1924  else if(dest=="-NaN")
1925  dest="-NAN";
1926  }
1927  }
1928  else if(type.id()==ID_fixedbv)
1929  {
1931 
1932  if(dest!="" && isdigit(dest[dest.size()-1]))
1933  {
1934  if(src.type()==float_type())
1935  dest+='f';
1936  else if(src.type()==long_double_type())
1937  dest+='l';
1938  }
1939  }
1940  else if(type.id()==ID_array ||
1941  type.id()==ID_incomplete_array)
1942  {
1943  dest=convert_array(src, precedence);
1944  }
1945  else if(type.id()==ID_pointer)
1946  {
1947  const irep_idt &value=to_constant_expr(src).get_value();
1948 
1949  if(value==ID_NULL)
1950  {
1951  dest="NULL";
1952  if(type.subtype().id()!=ID_empty)
1953  dest="(("+convert(type)+")"+dest+")";
1954  }
1955  else if(value==std::string(value.size(), '0') &&
1957  {
1958  dest="NULL";
1959  if(type.subtype().id()!=ID_empty)
1960  dest="(("+convert(type)+")"+dest+")";
1961  }
1962  else
1963  {
1964  // we prefer the annotation
1965  if(src.operands().size()!=1)
1966  return convert_norep(src, precedence);
1967 
1968  if(src.op0().id()==ID_constant)
1969  {
1970  const irep_idt &op_value=src.op0().get(ID_value);
1971 
1972  if(op_value=="INVALID" ||
1973  has_prefix(id2string(op_value), "INVALID-") ||
1974  op_value=="NULL+offset")
1975  dest=id2string(op_value);
1976  else
1977  return convert_norep(src, precedence);
1978  }
1979  else
1980  return convert_with_precedence(src.op0(), precedence);
1981  }
1982  }
1983  else if(type.id()==ID_string)
1984  {
1985  return '"'+id2string(src.get_value())+'"';
1986  }
1987  else
1988  return convert_norep(src, precedence);
1989 
1990  return dest;
1991 }
1992 
1997 std::string expr2ct::convert_constant_bool(bool boolean_value)
1998 {
1999  // C doesn't really have these
2000  if(boolean_value)
2001  return "TRUE";
2002  else
2003  return "FALSE";
2004 }
2005 
2007  const exprt &src,
2008  unsigned &precedence)
2009 {
2010  return convert_struct(src, precedence, true);
2011 }
2012 
2021  const exprt &src,
2022  unsigned &precedence,
2023  bool include_padding_components)
2024 {
2025  const typet full_type=ns.follow(src.type());
2026 
2027  if(full_type.id()!=ID_struct)
2028  return convert_norep(src, precedence);
2029 
2030  const struct_typet &struct_type=
2031  to_struct_type(full_type);
2032 
2033  const struct_typet::componentst &components=
2034  struct_type.components();
2035 
2036  if(components.size()!=src.operands().size())
2037  return convert_norep(src, precedence);
2038 
2039  std::string dest="{ ";
2040 
2041  exprt::operandst::const_iterator o_it=src.operands().begin();
2042 
2043  bool first=true;
2044  bool newline=false;
2045  size_t last_size=0;
2046 
2047  for(const struct_union_typet::componentt &component :
2048  struct_type.components())
2049  {
2050  if(o_it->type().id()==ID_code)
2051  continue;
2052 
2053  if(component.get_is_padding() && !include_padding_components)
2054  {
2055  ++o_it;
2056  continue;
2057  }
2058 
2059  if(first)
2060  first=false;
2061  else
2062  {
2063  dest+=',';
2064 
2065  if(newline)
2066  dest+="\n ";
2067  else
2068  dest+=' ';
2069  }
2070 
2071  std::string tmp=convert(*o_it);
2072 
2073  if(last_size+40<dest.size())
2074  {
2075  newline=true;
2076  last_size=dest.size();
2077  }
2078  else
2079  newline=false;
2080 
2081  dest+='.';
2082  dest+=component.get_string(ID_name);
2083  dest+='=';
2084  dest+=tmp;
2085 
2086  o_it++;
2087  }
2088 
2089  dest+=" }";
2090 
2091  return dest;
2092 }
2093 
2095  const exprt &src,
2096  unsigned &precedence)
2097 {
2098  const typet full_type=ns.follow(src.type());
2099 
2100  if(full_type.id()!=ID_vector)
2101  return convert_norep(src, precedence);
2102 
2103  std::string dest="{ ";
2104 
2105  bool first=true;
2106  bool newline=false;
2107  size_t last_size=0;
2108 
2109  forall_operands(it, src)
2110  {
2111  if(first)
2112  first=false;
2113  else
2114  {
2115  dest+=',';
2116 
2117  if(newline)
2118  dest+="\n ";
2119  else
2120  dest+=' ';
2121  }
2122 
2123  std::string tmp=convert(*it);
2124 
2125  if(last_size+40<dest.size())
2126  {
2127  newline=true;
2128  last_size=dest.size();
2129  }
2130  else
2131  newline=false;
2132 
2133  dest+=tmp;
2134  }
2135 
2136  dest+=" }";
2137 
2138  return dest;
2139 }
2140 
2142  const exprt &src,
2143  unsigned &precedence)
2144 {
2145  std::string dest="{ ";
2146 
2147  if(src.operands().size()!=1)
2148  return convert_norep(src, precedence);
2149 
2150  std::string tmp=convert(src.op0());
2151 
2152  dest+='.';
2153  dest+=src.get_string(ID_component_name);
2154  dest+='=';
2155  dest+=tmp;
2156 
2157  dest+=" }";
2158 
2159  return dest;
2160 }
2161 
2163  const exprt &src,
2164  unsigned &precedence)
2165 {
2166  std::string dest;
2167 
2168  // we treat arrays of characters as string constants,
2169  // and arrays of wchar_t as wide strings
2170 
2171  const typet &subtype=ns.follow(ns.follow(src.type()).subtype());
2172 
2173  bool all_constant=true;
2174 
2175  forall_operands(it, src)
2176  if(!it->is_constant())
2177  all_constant=false;
2178 
2179  if(src.get_bool(ID_C_string_constant) &&
2180  all_constant &&
2181  (subtype==char_type() || subtype==wchar_t_type()))
2182  {
2183  bool wide=subtype==wchar_t_type();
2184 
2185  if(wide)
2186  dest+='L';
2187 
2188  dest+="\"";
2189 
2190  dest.reserve(dest.size()+1+src.operands().size());
2191 
2192  bool last_was_hex=false;
2193 
2194  forall_operands(it, src)
2195  {
2196  // these have a trailing zero
2197  if(it==--src.operands().end())
2198  break;
2199 
2200  assert(it->is_constant());
2201  mp_integer i;
2202  to_integer(*it, i);
2203  unsigned int ch=integer2unsigned(i);
2204 
2205  if(last_was_hex)
2206  {
2207  // we use "string splicing" to avoid ambiguity
2208  if(isxdigit(ch))
2209  dest+="\" \"";
2210 
2211  last_was_hex=false;
2212  }
2213 
2214  switch(ch)
2215  {
2216  case '\n': dest+="\\n"; break; /* NL (0x0a) */
2217  case '\t': dest+="\\t"; break; /* HT (0x09) */
2218  case '\v': dest+="\\v"; break; /* VT (0x0b) */
2219  case '\b': dest+="\\b"; break; /* BS (0x08) */
2220  case '\r': dest+="\\r"; break; /* CR (0x0d) */
2221  case '\f': dest+="\\f"; break; /* FF (0x0c) */
2222  case '\a': dest+="\\a"; break; /* BEL (0x07) */
2223  case '\\': dest+="\\\\"; break;
2224  case '"': dest+="\\\""; break;
2225 
2226  default:
2227  if(ch>=' ' && ch!=127 && ch<0xff)
2228  dest+=static_cast<char>(ch);
2229  else
2230  {
2231  std::ostringstream oss;
2232  oss << "\\x" << std::hex << ch;
2233  dest += oss.str();
2234  last_was_hex=true;
2235  }
2236  }
2237  }
2238 
2239  dest+="\"";
2240 
2241  return dest;
2242  }
2243 
2244  dest="{ ";
2245 
2246  forall_operands(it, src)
2247  {
2248  std::string tmp;
2249 
2250  if(it->is_not_nil())
2251  tmp=convert(*it);
2252 
2253  if((it+1)!=src.operands().end())
2254  {
2255  tmp+=", ";
2256  if(tmp.size()>40)
2257  tmp+="\n ";
2258  }
2259 
2260  dest+=tmp;
2261  }
2262 
2263  dest+=" }";
2264 
2265  return dest;
2266 }
2267 
2269  const exprt &src,
2270  unsigned &precedence)
2271 {
2272  std::string dest="{ ";
2273 
2274  if((src.operands().size()%2)!=0)
2275  return convert_norep(src, precedence);
2276 
2277  forall_operands(it, src)
2278  {
2279  std::string tmp1=convert(*it);
2280 
2281  it++;
2282 
2283  std::string tmp2=convert(*it);
2284 
2285  std::string tmp="["+tmp1+"]="+tmp2;
2286 
2287  if((it+1)!=src.operands().end())
2288  {
2289  tmp+=", ";
2290  if(tmp.size()>40)
2291  tmp+="\n ";
2292  }
2293 
2294  dest+=tmp;
2295  }
2296 
2297  dest+=" }";
2298 
2299  return dest;
2300 }
2301 
2303  const exprt &src,
2304  unsigned &precedence)
2305 {
2306  std::string dest;
2307  if(src.id()!=ID_compound_literal)
2308  dest+="{ ";
2309 
2310  forall_operands(it, src)
2311  {
2312  std::string tmp=convert(*it);
2313 
2314  if((it+1)!=src.operands().end())
2315  {
2316  tmp+=", ";
2317  if(tmp.size()>40)
2318  tmp+="\n ";
2319  }
2320 
2321  dest+=tmp;
2322  }
2323 
2324  if(src.id()!=ID_compound_literal)
2325  dest+=" }";
2326 
2327  return dest;
2328 }
2329 
2331  const exprt &src,
2332  unsigned &precedence)
2333 {
2334  if(src.operands().size()!=1)
2335  {
2336  unsigned precedence;
2337  return convert_norep(src, precedence);
2338  }
2339 
2340  std::string dest=".";
2341  // TODO it->find(ID_member)
2342  dest+='=';
2343  dest+=convert(src.op0());
2344 
2345  return dest;
2346 }
2347 
2349  const function_application_exprt &src,
2350  unsigned &precedence)
2351 {
2352  std::string dest;
2353 
2354  {
2355  unsigned p;
2356  std::string function_str=convert_with_precedence(src.function(), p);
2357  dest+=function_str;
2358  }
2359 
2360  dest+='(';
2361 
2362  forall_expr(it, src.arguments())
2363  {
2364  unsigned p;
2365  std::string arg_str=convert_with_precedence(*it, p);
2366 
2367  if(it!=src.arguments().begin())
2368  dest+=", ";
2369  // TODO: ggf. Klammern je nach p
2370  dest+=arg_str;
2371  }
2372 
2373  dest+=')';
2374 
2375  return dest;
2376 }
2377 
2380  unsigned &precedence)
2381 {
2382  std::string dest;
2383 
2384  {
2385  unsigned p;
2386  std::string function_str=convert_with_precedence(src.function(), p);
2387  dest+=function_str;
2388  }
2389 
2390  dest+='(';
2391 
2392  forall_expr(it, src.arguments())
2393  {
2394  unsigned p;
2395  std::string arg_str=convert_with_precedence(*it, p);
2396 
2397  if(it!=src.arguments().begin())
2398  dest+=", ";
2399  // TODO: ggf. Klammern je nach p
2400  dest+=arg_str;
2401  }
2402 
2403  dest+=')';
2404 
2405  return dest;
2406 }
2407 
2409  const exprt &src,
2410  unsigned &precedence)
2411 {
2412  precedence=16;
2413 
2414  std::string dest="overflow(\"";
2415  dest+=src.id().c_str()+9;
2416  dest+="\"";
2417 
2418  if(!src.operands().empty())
2419  {
2420  dest+=", ";
2421  dest+=convert(src.op0().type());
2422  }
2423 
2424  forall_operands(it, src)
2425  {
2426  unsigned p;
2427  std::string arg_str=convert_with_precedence(*it, p);
2428 
2429  dest+=", ";
2430  // TODO: ggf. Klammern je nach p
2431  dest+=arg_str;
2432  }
2433 
2434  dest+=')';
2435 
2436  return dest;
2437 }
2438 
2439 std::string expr2ct::indent_str(unsigned indent)
2440 {
2441  return std::string(indent, ' ');
2442 }
2443 
2445  const code_asmt &src,
2446  unsigned indent)
2447 {
2448  std::string dest=indent_str(indent);
2449 
2450  if(src.get_flavor()==ID_gcc)
2451  {
2452  if(src.operands().size()==5)
2453  {
2454  dest+="asm(";
2455  dest+=convert(src.op0());
2456  if(!src.operands()[1].operands().empty() ||
2457  !src.operands()[2].operands().empty() ||
2458  !src.operands()[3].operands().empty() ||
2459  !src.operands()[4].operands().empty())
2460  {
2461  // need extended syntax
2462 
2463  // outputs
2464  dest+=" : ";
2465  forall_operands(it, src.op1())
2466  {
2467  if(it->operands().size()==2)
2468  {
2469  if(it!=src.op1().operands().begin())
2470  dest+=", ";
2471  dest+=convert(it->op0());
2472  dest+="(";
2473  dest+=convert(it->op1());
2474  dest+=")";
2475  }
2476  }
2477 
2478  // inputs
2479  dest+=" : ";
2480  forall_operands(it, src.op2())
2481  {
2482  if(it->operands().size()==2)
2483  {
2484  if(it!=src.op2().operands().begin())
2485  dest+=", ";
2486  dest+=convert(it->op0());
2487  dest+="(";
2488  dest+=convert(it->op1());
2489  dest+=")";
2490  }
2491  }
2492 
2493  // clobbered registers
2494  dest+=" : ";
2495  forall_operands(it, src.op3())
2496  {
2497  if(it!=src.op3().operands().begin())
2498  dest+=", ";
2499  if(it->id()==ID_gcc_asm_clobbered_register)
2500  dest+=convert(it->op0());
2501  else
2502  dest+=convert(*it);
2503  }
2504  }
2505  dest+=");";
2506  }
2507  }
2508  else if(src.get_flavor()==ID_msc)
2509  {
2510  if(src.operands().size()==1)
2511  {
2512  dest+="__asm {\n";
2513  dest+=indent_str(indent);
2514  dest+=convert(src.op0());
2515  dest+="\n}";
2516  }
2517  }
2518 
2519  return dest;
2520 }
2521 
2523  const code_whilet &src,
2524  unsigned indent)
2525 {
2526  if(src.operands().size()!=2)
2527  {
2528  unsigned precedence;
2529  return convert_norep(src, precedence);
2530  }
2531 
2532  std::string dest=indent_str(indent);
2533  dest+="while("+convert(src.cond());
2534 
2535  if(src.body().is_nil())
2536  dest+=");";
2537  else
2538  {
2539  dest+=")\n";
2540  dest+=convert_code(
2541  src.body(),
2542  src.body().get_statement()==ID_block ? indent : indent+2);
2543  }
2544 
2545  return dest;
2546 }
2547 
2549  const code_dowhilet &src,
2550  unsigned indent)
2551 {
2552  if(src.operands().size()!=2)
2553  {
2554  unsigned precedence;
2555  return convert_norep(src, precedence);
2556  }
2557 
2558  std::string dest=indent_str(indent);
2559 
2560  if(src.body().is_nil())
2561  dest+="do;";
2562  else
2563  {
2564  dest+="do\n";
2565  dest+=convert_code(
2566  src.body(),
2567  src.body().get_statement()==ID_block ? indent : indent+2);
2568  dest+="\n";
2569  dest+=indent_str(indent);
2570  }
2571 
2572  dest+="while("+convert(src.cond())+");";
2573 
2574  return dest;
2575 }
2576 
2578  const code_ifthenelset &src,
2579  unsigned indent)
2580 {
2581  if(src.operands().size()!=3)
2582  {
2583  unsigned precedence;
2584  return convert_norep(src, precedence);
2585  }
2586 
2587  std::string dest=indent_str(indent);
2588  dest+="if("+convert(src.cond())+")\n";
2589 
2590  if(src.then_case().is_nil())
2591  {
2592  dest+=indent_str(indent+2);
2593  dest+=';';
2594  }
2595  else
2596  dest += convert_code(
2597  src.then_case(),
2598  src.then_case().get_statement() == ID_block ? indent : indent + 2);
2599  dest+="\n";
2600 
2601  if(!src.else_case().is_nil())
2602  {
2603  dest+="\n";
2604  dest+=indent_str(indent);
2605  dest+="else\n";
2606  dest += convert_code(
2607  src.else_case(),
2608  src.else_case().get_statement() == ID_block ? indent : indent + 2);
2609  }
2610 
2611  return dest;
2612 }
2613 
2615  const codet &src,
2616  unsigned indent)
2617 {
2618  if(!src.operands().empty() &&
2619  src.operands().size()!=1)
2620  {
2621  unsigned precedence;
2622  return convert_norep(src, precedence);
2623  }
2624 
2625  std::string dest=indent_str(indent);
2626  dest+="return";
2627 
2628  if(to_code_return(src).has_return_value())
2629  dest+=" "+convert(src.op0());
2630 
2631  dest+=';';
2632 
2633  return dest;
2634 }
2635 
2637  const codet &src,
2638  unsigned indent)
2639 {
2640  std:: string dest=indent_str(indent);
2641  dest+="goto ";
2642  dest+=clean_identifier(src.get(ID_destination));
2643  dest+=';';
2644 
2645  return dest;
2646 }
2647 
2649  const codet &src,
2650  unsigned indent)
2651 {
2652  std::string dest=indent_str(indent);
2653  dest+="break";
2654  dest+=';';
2655 
2656  return dest;
2657 }
2658 
2660  const codet &src,
2661  unsigned indent)
2662 {
2663  if(src.operands().empty())
2664  {
2665  unsigned precedence;
2666  return convert_norep(src, precedence);
2667  }
2668 
2669  std::string dest=indent_str(indent);
2670  dest+="switch(";
2671  dest+=convert(src.op0());
2672  dest+=")\n";
2673 
2674  dest+=indent_str(indent);
2675  dest+='{';
2676 
2677  forall_operands(it, src)
2678  {
2679  if(it==src.operands().begin())
2680  continue;
2681  const exprt &op=*it;
2682 
2683  if(op.get(ID_statement)!=ID_block)
2684  {
2685  unsigned precedence;
2686  dest+=convert_norep(op, precedence);
2687  }
2688  else
2689  {
2690  forall_operands(it2, op)
2691  dest+=convert_code(to_code(*it2), indent+2);
2692  }
2693  }
2694 
2695  dest+="\n";
2696  dest+=indent_str(indent);
2697  dest+='}';
2698 
2699  return dest;
2700 }
2701 
2703  const codet &src,
2704  unsigned indent)
2705 {
2706  std::string dest=indent_str(indent);
2707  dest+="continue";
2708  dest+=';';
2709 
2710  return dest;
2711 }
2712 
2714  const codet &src,
2715  unsigned indent)
2716 {
2717  // initializer to go away
2718  if(src.operands().size()!=1 &&
2719  src.operands().size()!=2)
2720  {
2721  unsigned precedence;
2722  return convert_norep(src, precedence);
2723  }
2724 
2725  std::string declarator=convert(src.op0());
2726 
2727  std::string dest=indent_str(indent);
2728 
2729  const symbolt *symbol=nullptr;
2730  if(!ns.lookup(to_symbol_expr(src.op0()).get_identifier(), symbol))
2731  {
2732  if(symbol->is_file_local &&
2733  (src.op0().type().id()==ID_code || symbol->is_static_lifetime))
2734  dest+="static ";
2735  else if(symbol->is_extern)
2736  dest+="extern ";
2737  else if(
2739  {
2740  dest += "__declspec(dllexport) ";
2741  }
2742 
2743  if(symbol->type.id()==ID_code &&
2744  to_code_type(symbol->type).get_inlined())
2745  dest+="inline ";
2746  }
2747 
2748  dest+=convert_rec(src.op0().type(), c_qualifierst(), declarator);
2749 
2750  if(src.operands().size()==2)
2751  dest+="="+convert(src.op1());
2752 
2753  dest+=';';
2754 
2755  return dest;
2756 }
2757 
2759  const codet &src,
2760  unsigned indent)
2761 {
2762  // initializer to go away
2763  if(src.operands().size()!=1)
2764  {
2765  unsigned precedence;
2766  return convert_norep(src, precedence);
2767  }
2768 
2769  return indent_str(indent) + "dead " + convert(src.op0()) + ";";
2770 }
2771 
2773  const code_fort &src,
2774  unsigned indent)
2775 {
2776  if(src.operands().size()!=4)
2777  {
2778  unsigned precedence;
2779  return convert_norep(src, precedence);
2780  }
2781 
2782  std::string dest=indent_str(indent);
2783  dest+="for(";
2784 
2785  if(!src.op0().is_nil())
2786  dest+=convert(src.op0());
2787  else
2788  dest+=' ';
2789  dest+="; ";
2790  if(!src.op1().is_nil())
2791  dest+=convert(src.op1());
2792  dest+="; ";
2793  if(!src.op2().is_nil())
2794  dest+=convert(src.op2());
2795 
2796  if(src.body().is_nil())
2797  dest+=");\n";
2798  else
2799  {
2800  dest+=")\n";
2801  dest+=convert_code(
2802  src.body(),
2803  src.body().get_statement()==ID_block ? indent : indent+2);
2804  }
2805 
2806  return dest;
2807 }
2808 
2810  const code_blockt &src,
2811  unsigned indent)
2812 {
2813  std::string dest=indent_str(indent);
2814  dest+="{\n";
2815 
2816  forall_operands(it, src)
2817  {
2818  if(it->get(ID_statement)==ID_label)
2819  dest+=convert_code(to_code(*it), indent);
2820  else
2821  dest+=convert_code(to_code(*it), indent+2);
2822 
2823  dest+="\n";
2824  }
2825 
2826  dest+=indent_str(indent);
2827  dest+='}';
2828 
2829  return dest;
2830 }
2831 
2833  const codet &src,
2834  unsigned indent)
2835 {
2836  std::string dest;
2837 
2838  forall_operands(it, src)
2839  {
2840  dest+=convert_code(to_code(*it), indent);
2841  dest+="\n";
2842  }
2843 
2844  return dest;
2845 }
2846 
2848  const codet &src,
2849  unsigned indent)
2850 {
2851  std::string dest=indent_str(indent);
2852 
2853  std::string expr_str;
2854  if(src.operands().size()==1)
2855  expr_str=convert(src.op0());
2856  else
2857  {
2858  unsigned precedence;
2859  expr_str=convert_norep(src, precedence);
2860  }
2861 
2862  dest+=expr_str;
2863  if(dest.empty() || *dest.rbegin()!=';')
2864  dest+=';';
2865 
2866  return dest;
2867 }
2868 
2870  const codet &src,
2871  unsigned indent)
2872 {
2873  static bool comment_done=false;
2874 
2875  if(!comment_done && !src.source_location().get_comment().empty())
2876  {
2877  comment_done=true;
2878  std::string dest=indent_str(indent);
2879  dest+="/* "+id2string(src.source_location().get_comment())+" */\n";
2880  dest+=convert_code(src, indent);
2881  comment_done=false;
2882  return dest;
2883  }
2884 
2885  const irep_idt &statement=src.get_statement();
2886 
2887  if(statement==ID_expression)
2888  return convert_code_expression(src, indent);
2889 
2890  if(statement==ID_block)
2891  return convert_code_block(to_code_block(src), indent);
2892 
2893  if(statement==ID_switch)
2894  return convert_code_switch(src, indent);
2895 
2896  if(statement==ID_for)
2897  return convert_code_for(to_code_for(src), indent);
2898 
2899  if(statement==ID_while)
2900  return convert_code_while(to_code_while(src), indent);
2901 
2902  if(statement==ID_asm)
2903  return convert_code_asm(to_code_asm(src), indent);
2904 
2905  if(statement==ID_skip)
2906  return indent_str(indent)+";";
2907 
2908  if(statement==ID_dowhile)
2909  return convert_code_dowhile(to_code_dowhile(src), indent);
2910 
2911  if(statement==ID_ifthenelse)
2912  return convert_code_ifthenelse(to_code_ifthenelse(src), indent);
2913 
2914  if(statement==ID_return)
2915  return convert_code_return(src, indent);
2916 
2917  if(statement==ID_goto)
2918  return convert_code_goto(src, indent);
2919 
2920  if(statement==ID_printf)
2921  return convert_code_printf(src, indent);
2922 
2923  if(statement==ID_fence)
2924  return convert_code_fence(src, indent);
2925 
2926  if(statement==ID_input)
2927  return convert_code_input(src, indent);
2928 
2929  if(statement==ID_output)
2930  return convert_code_output(src, indent);
2931 
2932  if(statement==ID_assume)
2933  return convert_code_assume(src, indent);
2934 
2935  if(statement==ID_assert)
2936  return convert_code_assert(src, indent);
2937 
2938  if(statement==ID_break)
2939  return convert_code_break(src, indent);
2940 
2941  if(statement==ID_continue)
2942  return convert_code_continue(src, indent);
2943 
2944  if(statement==ID_decl)
2945  return convert_code_decl(src, indent);
2946 
2947  if(statement==ID_decl_block)
2948  return convert_code_decl_block(src, indent);
2949 
2950  if(statement==ID_dead)
2951  return convert_code_dead(src, indent);
2952 
2953  if(statement==ID_assign)
2954  return convert_code_assign(to_code_assign(src), indent);
2955 
2956  if(statement==ID_init)
2957  return convert_code_init(src, indent);
2958 
2959  if(statement=="lock")
2960  return convert_code_lock(src, indent);
2961 
2962  if(statement=="unlock")
2963  return convert_code_unlock(src, indent);
2964 
2965  if(statement==ID_atomic_begin)
2966  return indent_str(indent)+"__CPROVER_atomic_begin();";
2967 
2968  if(statement==ID_atomic_end)
2969  return indent_str(indent)+"__CPROVER_atomic_end();";
2970 
2971  if(statement==ID_function_call)
2973 
2974  if(statement==ID_label)
2975  return convert_code_label(to_code_label(src), indent);
2976 
2977  if(statement==ID_switch_case)
2978  return convert_code_switch_case(to_code_switch_case(src), indent);
2979 
2980  if(statement==ID_free)
2981  return convert_code_free(src, indent);
2982 
2983  if(statement==ID_array_set)
2984  return convert_code_array_set(src, indent);
2985 
2986  if(statement==ID_array_copy)
2987  return convert_code_array_copy(src, indent);
2988 
2989  if(statement==ID_array_replace)
2990  return convert_code_array_replace(src, indent);
2991 
2992  if(statement=="set_may" ||
2993  statement=="set_must")
2994  return
2995  indent_str(indent)+convert_function(src, id2string(statement), 16)+";";
2996 
2997  unsigned precedence;
2998  return convert_norep(src, precedence);
2999 }
3000 
3002  const code_assignt &src,
3003  unsigned indent)
3004 {
3005  std::string tmp=convert_binary(src, "=", 2, true);
3006 
3007  std::string dest=indent_str(indent)+tmp+";";
3008 
3009  return dest;
3010 }
3011 
3013  const codet &src,
3014  unsigned indent)
3015 {
3016  if(src.operands().size()!=1)
3017  {
3018  unsigned precedence;
3019  return convert_norep(src, precedence);
3020  }
3021 
3022  return indent_str(indent)+"FREE("+convert(src.op0())+");";
3023 }
3024 
3026  const codet &src,
3027  unsigned indent)
3028 {
3029  std::string tmp=convert_binary(src, "=", 2, true);
3030 
3031  return indent_str(indent)+"INIT "+tmp+";";
3032 }
3033 
3035  const codet &src,
3036  unsigned indent)
3037 {
3038  if(src.operands().size()!=1)
3039  {
3040  unsigned precedence;
3041  return convert_norep(src, precedence);
3042  }
3043 
3044  return indent_str(indent)+"LOCK("+convert(src.op0())+");";
3045 }
3046 
3048  const codet &src,
3049  unsigned indent)
3050 {
3051  if(src.operands().size()!=1)
3052  {
3053  unsigned precedence;
3054  return convert_norep(src, precedence);
3055  }
3056 
3057  return indent_str(indent)+"UNLOCK("+convert(src.op0())+");";
3058 }
3059 
3061  const code_function_callt &src,
3062  unsigned indent)
3063 {
3064  if(src.operands().size()!=3)
3065  {
3066  unsigned precedence;
3067  return convert_norep(src, precedence);
3068  }
3069 
3070  std::string dest=indent_str(indent);
3071 
3072  if(src.lhs().is_not_nil())
3073  {
3074  unsigned p;
3075  std::string lhs_str=convert_with_precedence(src.lhs(), p);
3076 
3077  // TODO: ggf. Klammern je nach p
3078  dest+=lhs_str;
3079  dest+='=';
3080  }
3081 
3082  {
3083  unsigned p;
3084  std::string function_str=convert_with_precedence(src.function(), p);
3085  dest+=function_str;
3086  }
3087 
3088  dest+='(';
3089 
3090  const exprt::operandst &arguments=src.arguments();
3091 
3092  forall_expr(it, arguments)
3093  {
3094  unsigned p;
3095  std::string arg_str=convert_with_precedence(*it, p);
3096 
3097  if(it!=arguments.begin())
3098  dest+=", ";
3099  // TODO: ggf. Klammern je nach p
3100  dest+=arg_str;
3101  }
3102 
3103  dest+=");";
3104 
3105  return dest;
3106 }
3107 
3109  const codet &src,
3110  unsigned indent)
3111 {
3112  std::string dest=indent_str(indent)+"printf(";
3113 
3114  forall_operands(it, src)
3115  {
3116  unsigned p;
3117  std::string arg_str=convert_with_precedence(*it, p);
3118 
3119  if(it!=src.operands().begin())
3120  dest+=", ";
3121  // TODO: ggf. Klammern je nach p
3122  dest+=arg_str;
3123  }
3124 
3125  dest+=");";
3126 
3127  return dest;
3128 }
3129 
3131  const codet &src,
3132  unsigned indent)
3133 {
3134  std::string dest=indent_str(indent)+"FENCE(";
3135 
3136  irep_idt att[]=
3137  { ID_WRfence, ID_RRfence, ID_RWfence, ID_WWfence,
3138  ID_RRcumul, ID_RWcumul, ID_WWcumul, ID_WRcumul,
3139  irep_idt() };
3140 
3141  bool first=true;
3142 
3143  for(unsigned i=0; !att[i].empty(); i++)
3144  {
3145  if(src.get_bool(att[i]))
3146  {
3147  if(first)
3148  first=false;
3149  else
3150  dest+='+';
3151 
3152  dest+=id2string(att[i]);
3153  }
3154  }
3155 
3156  dest+=");";
3157  return dest;
3158 }
3159 
3161  const codet &src,
3162  unsigned indent)
3163 {
3164  std::string dest=indent_str(indent)+"INPUT(";
3165 
3166  forall_operands(it, src)
3167  {
3168  unsigned p;
3169  std::string arg_str=convert_with_precedence(*it, p);
3170 
3171  if(it!=src.operands().begin())
3172  dest+=", ";
3173  // TODO: ggf. Klammern je nach p
3174  dest+=arg_str;
3175  }
3176 
3177  dest+=");";
3178 
3179  return dest;
3180 }
3181 
3183  const codet &src,
3184  unsigned indent)
3185 {
3186  std::string dest=indent_str(indent)+"OUTPUT(";
3187 
3188  forall_operands(it, src)
3189  {
3190  unsigned p;
3191  std::string arg_str=convert_with_precedence(*it, p);
3192 
3193  if(it!=src.operands().begin())
3194  dest+=", ";
3195  dest+=arg_str;
3196  }
3197 
3198  dest+=");";
3199 
3200  return dest;
3201 }
3202 
3204  const codet &src,
3205  unsigned indent)
3206 {
3207  std::string dest=indent_str(indent)+"ARRAY_SET(";
3208 
3209  forall_operands(it, src)
3210  {
3211  unsigned p;
3212  std::string arg_str=convert_with_precedence(*it, p);
3213 
3214  if(it!=src.operands().begin())
3215  dest+=", ";
3216  // TODO: ggf. Klammern je nach p
3217  dest+=arg_str;
3218  }
3219 
3220  dest+=");";
3221 
3222  return dest;
3223 }
3224 
3226  const codet &src,
3227  unsigned indent)
3228 {
3229  std::string dest=indent_str(indent)+"ARRAY_COPY(";
3230 
3231  forall_operands(it, src)
3232  {
3233  unsigned p;
3234  std::string arg_str=convert_with_precedence(*it, p);
3235 
3236  if(it!=src.operands().begin())
3237  dest+=", ";
3238  // TODO: ggf. Klammern je nach p
3239  dest+=arg_str;
3240  }
3241 
3242  dest+=");";
3243 
3244  return dest;
3245 }
3246 
3248  const codet &src,
3249  unsigned indent)
3250 {
3251  std::string dest=indent_str(indent)+"ARRAY_REPLACE(";
3252 
3253  forall_operands(it, src)
3254  {
3255  unsigned p;
3256  std::string arg_str=convert_with_precedence(*it, p);
3257 
3258  if(it!=src.operands().begin())
3259  dest+=", ";
3260  dest+=arg_str;
3261  }
3262 
3263  dest+=");";
3264 
3265  return dest;
3266 }
3267 
3269  const codet &src,
3270  unsigned indent)
3271 {
3272  if(src.operands().size()!=1)
3273  {
3274  unsigned precedence;
3275  return convert_norep(src, precedence);
3276  }
3277 
3278  return indent_str(indent)+"assert("+convert(src.op0())+");";
3279 }
3280 
3282  const codet &src,
3283  unsigned indent)
3284 {
3285  if(src.operands().size()!=1)
3286  {
3287  unsigned precedence;
3288  return convert_norep(src, precedence);
3289  }
3290 
3291  return indent_str(indent)+"__CPROVER_assume("+convert(src.op0())+");";
3292 }
3293 
3295  const code_labelt &src,
3296  unsigned indent)
3297 {
3298  std::string labels_string;
3299 
3300  irep_idt label=src.get_label();
3301 
3302  labels_string+="\n";
3303  labels_string+=indent_str(indent);
3304  labels_string+=clean_identifier(label);
3305  labels_string+=":\n";
3306 
3307  std::string tmp=convert_code(src.code(), indent+2);
3308 
3309  return labels_string+tmp;
3310 }
3311 
3313  const code_switch_caset &src,
3314  unsigned indent)
3315 {
3316  std::string labels_string;
3317 
3318  if(src.is_default())
3319  {
3320  labels_string+="\n";
3321  labels_string+=indent_str(indent);
3322  labels_string+="default:\n";
3323  }
3324  else
3325  {
3326  labels_string+="\n";
3327  labels_string+=indent_str(indent);
3328  labels_string+="case ";
3329  labels_string+=convert(src.case_op());
3330  labels_string+=":\n";
3331  }
3332 
3333  unsigned next_indent=indent;
3334  if(src.code().get_statement()!=ID_block &&
3335  src.code().get_statement()!=ID_switch_case)
3336  next_indent+=2;
3337  std::string tmp=convert_code(src.code(), next_indent);
3338 
3339  return labels_string+tmp;
3340 }
3341 
3342 std::string expr2ct::convert_code(const codet &src)
3343 {
3344  return convert_code(src, 0);
3345 }
3346 
3347 std::string expr2ct::convert_Hoare(const exprt &src)
3348 {
3349  unsigned precedence;
3350 
3351  if(src.operands().size()!=2)
3352  return convert_norep(src, precedence);
3353 
3354  const exprt &assumption=src.op0();
3355  const exprt &assertion=src.op1();
3356  const codet &code=
3357  static_cast<const codet &>(src.find(ID_code));
3358 
3359  std::string dest="\n";
3360  dest+='{';
3361 
3362  if(!assumption.is_nil())
3363  {
3364  std::string assumption_str=convert(assumption);
3365  dest+=" assume(";
3366  dest+=assumption_str;
3367  dest+=");\n";
3368  }
3369  else
3370  dest+="\n";
3371 
3372  {
3373  std::string code_str=convert_code(code);
3374  dest+=code_str;
3375  }
3376 
3377  if(!assertion.is_nil())
3378  {
3379  std::string assertion_str=convert(assertion);
3380  dest+=" assert(";
3381  dest+=assertion_str;
3382  dest+=");\n";
3383  }
3384 
3385  dest+='}';
3386 
3387  return dest;
3388 }
3389 
3391  const exprt &src,
3392  unsigned precedence)
3393 {
3394  if(src.operands().size()!=2)
3395  return convert_norep(src, precedence);
3396 
3397  std::string dest=convert_with_precedence(src.op0(), precedence);
3398  dest+='[';
3399  dest+=convert_with_precedence(src.op1(), precedence);
3400  dest+=']';
3401 
3402  return dest;
3403 }
3404 
3406  const exprt &src,
3407  unsigned precedence)
3408 {
3409  if(src.operands().size()!=3)
3410  return convert_norep(src, precedence);
3411 
3412  std::string dest=convert_with_precedence(src.op0(), precedence);
3413  dest+='[';
3414  dest+=convert_with_precedence(src.op1(), precedence);
3415  dest+=", ";
3416  dest+=convert_with_precedence(src.op2(), precedence);
3417  dest+=']';
3418 
3419  return dest;
3420 }
3421 
3423  const exprt &src,
3424  unsigned &precedence)
3425 {
3426  if(src.has_operands())
3427  return convert_norep(src, precedence);
3428 
3429  std::string dest="sizeof(";
3430  dest+=convert(static_cast<const typet&>(src.find(ID_type_arg)));
3431  dest+=')';
3432 
3433  return dest;
3434 }
3435 
3437  const exprt &src,
3438  unsigned &precedence)
3439 {
3440  precedence=16;
3441 
3442  if(src.id()==ID_plus)
3443  return convert_multi_ary(src, "+", precedence=12, false);
3444 
3445  else if(src.id()==ID_minus)
3446  return convert_binary(src, "-", precedence=12, true);
3447 
3448  else if(src.id()==ID_unary_minus)
3449  return convert_unary(src, "-", precedence=15);
3450 
3451  else if(src.id()==ID_unary_plus)
3452  return convert_unary(src, "+", precedence=15);
3453 
3454  else if(src.id()==ID_floatbv_plus)
3455  return convert_function(src, "FLOAT+", precedence=16);
3456 
3457  else if(src.id()==ID_floatbv_minus)
3458  return convert_function(src, "FLOAT-", precedence=16);
3459 
3460  else if(src.id()==ID_floatbv_mult)
3461  return convert_function(src, "FLOAT*", precedence=16);
3462 
3463  else if(src.id()==ID_floatbv_div)
3464  return convert_function(src, "FLOAT/", precedence=16);
3465 
3466  else if(src.id()==ID_floatbv_rem)
3467  return convert_function(src, "FLOAT%", precedence=16);
3468 
3469  else if(src.id()==ID_floatbv_typecast)
3470  {
3471  precedence=16;
3472  std::string dest="FLOAT_TYPECAST(";
3473 
3474  unsigned p0;
3475  std::string tmp0=convert_with_precedence(src.op0(), p0);
3476 
3477  if(p0<=1)
3478  dest+='(';
3479  dest+=tmp0;
3480  if(p0<=1)
3481  dest+=')';
3482 
3483  const typet &to_type=ns.follow(src.type());
3484  dest+=", ";
3485  dest+=convert(to_type);
3486  dest+=", ";
3487 
3488  unsigned p1;
3489  std::string tmp1=convert_with_precedence(src.op1(), p1);
3490 
3491  if(p1<=1)
3492  dest+='(';
3493  dest+=tmp1;
3494  if(p1<=1)
3495  dest+=')';
3496 
3497  dest+=')';
3498  return dest;
3499  }
3500 
3501  else if(src.id()==ID_sign)
3502  {
3503  if(src.operands().size()==1 &&
3504  src.op0().type().id()==ID_floatbv)
3505  return convert_function(src, "signbit", precedence=16);
3506  else
3507  return convert_function(src, "SIGN", precedence=16);
3508  }
3509 
3510  else if(src.id()==ID_popcount)
3511  {
3513  return convert_function(src, "__popcnt", precedence=16);
3514  else
3515  return convert_function(src, "__builtin_popcount", precedence=16);
3516  }
3517 
3518  else if(src.id() == ID_r_ok)
3519  return convert_function(src, "R_OK", precedence = 16);
3520 
3521  else if(src.id() == ID_w_ok)
3522  return convert_function(src, "W_OK", precedence = 16);
3523 
3524  else if(src.id()==ID_invalid_pointer)
3525  return convert_function(src, "INVALID-POINTER", precedence=16);
3526 
3527  else if(src.id()==ID_good_pointer)
3528  return convert_function(src, "GOOD_POINTER", precedence=16);
3529 
3530  else if(src.id()==ID_object_size)
3531  return convert_function(src, "OBJECT_SIZE", precedence=16);
3532 
3533  else if(src.id()=="pointer_arithmetic")
3534  return convert_pointer_arithmetic(src, precedence=16);
3535 
3536  else if(src.id()=="pointer_difference")
3537  return convert_pointer_difference(src, precedence=16);
3538 
3539  else if(src.id() == ID_null_object)
3540  return "NULL-object";
3541 
3542  else if(src.id()==ID_integer_address ||
3543  src.id()==ID_integer_address_object ||
3544  src.id()==ID_stack_object ||
3545  src.id()==ID_static_object)
3546  {
3547  return id2string(src.id());
3548  }
3549 
3550  else if(src.id()==ID_infinity)
3551  return convert_function(src, "INFINITY", precedence=16);
3552 
3553  else if(src.id()=="builtin-function")
3554  return src.get_string(ID_identifier);
3555 
3556  else if(src.id()==ID_pointer_object)
3557  return convert_function(src, "POINTER_OBJECT", precedence=16);
3558 
3559  else if(src.id()=="get_must")
3560  return convert_function(src, "__CPROVER_get_must", precedence=16);
3561 
3562  else if(src.id()=="get_may")
3563  return convert_function(src, "__CPROVER_get_may", precedence=16);
3564 
3565  else if(src.id()=="object_value")
3566  return convert_function(src, "OBJECT_VALUE", precedence=16);
3567 
3568  else if(src.id()==ID_array_of)
3569  return convert_array_of(src, precedence=16);
3570 
3571  else if(src.id()==ID_pointer_offset)
3572  return convert_function(src, "POINTER_OFFSET", precedence=16);
3573 
3574  else if(src.id()=="pointer_base")
3575  return convert_function(src, "POINTER_BASE", precedence=16);
3576 
3577  else if(src.id()=="pointer_cons")
3578  return convert_function(src, "POINTER_CONS", precedence=16);
3579 
3580  else if(src.id()==ID_invalid_pointer)
3581  return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);
3582 
3583  else if(src.id()==ID_dynamic_object)
3584  return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
3585 
3586  else if(src.id()=="is_zero_string")
3587  return convert_function(src, "IS_ZERO_STRING", precedence=16);
3588 
3589  else if(src.id()=="zero_string")
3590  return convert_function(src, "ZERO_STRING", precedence=16);
3591 
3592  else if(src.id()=="zero_string_length")
3593  return convert_function(src, "ZERO_STRING_LENGTH", precedence=16);
3594 
3595  else if(src.id()=="buffer_size")
3596  return convert_function(src, "BUFFER_SIZE", precedence=16);
3597 
3598  else if(src.id()==ID_isnan)
3599  return convert_function(src, "isnan", precedence=16);
3600 
3601  else if(src.id()==ID_isfinite)
3602  return convert_function(src, "isfinite", precedence=16);
3603 
3604  else if(src.id()==ID_isinf)
3605  return convert_function(src, "isinf", precedence=16);
3606 
3607  else if(src.id()==ID_bswap)
3608  return convert_function(
3609  src,
3610  "__builtin_bswap"+
3612  precedence=16);
3613 
3614  else if(src.id()==ID_isnormal)
3615  return convert_function(src, "isnormal", precedence=16);
3616 
3617  else if(src.id()==ID_builtin_offsetof)
3618  return convert_function(src, "builtin_offsetof", precedence=16);
3619 
3620  else if(src.id()==ID_gcc_builtin_va_arg)
3621  return convert_function(src, "gcc_builtin_va_arg", precedence=16);
3622 
3623  else if(src.id()==ID_alignof)
3624  // C uses "_Alignof", C++ uses "alignof"
3625  return convert_function(src, "alignof", precedence=16);
3626 
3627  else if(has_prefix(src.id_string(), "byte_extract"))
3628  return convert_byte_extract(src, precedence=16);
3629 
3630  else if(has_prefix(src.id_string(), "byte_update"))
3631  return convert_byte_update(src, precedence=16);
3632 
3633  else if(src.id()==ID_address_of)
3634  {
3635  if(src.operands().size()!=1)
3636  return convert_norep(src, precedence);
3637  else if(src.op0().id()==ID_label)
3638  return "&&"+src.op0().get_string(ID_identifier);
3639  else if(src.op0().id()==ID_index &&
3640  to_index_expr(src.op0()).index().is_zero())
3641  return convert(to_index_expr(src.op0()).array());
3642  else if(src.type().subtype().id()==ID_code)
3643  return convert_unary(src, "", precedence=15);
3644  else
3645  return convert_unary(src, "&", precedence=15);
3646  }
3647 
3648  else if(src.id()==ID_dereference)
3649  {
3650  if(src.operands().size()!=1)
3651  return convert_norep(src, precedence);
3652  else if(src.type().id()==ID_code)
3653  return convert_unary(src, "", precedence=15);
3654  else if(src.op0().id()==ID_plus &&
3655  src.op0().operands().size()==2 &&
3656  ns.follow(src.op0().op0().type()).id()==ID_pointer)
3657  {
3658  // Note that index[pointer] is legal C, but we avoid it nevertheless.
3659  return convert(index_exprt(src.op0().op0(), src.op0().op1()));
3660  }
3661  else
3662  return convert_unary(src, "*", precedence=15);
3663  }
3664 
3665  else if(src.id()==ID_index)
3666  return convert_index(src, precedence=16);
3667 
3668  else if(src.id()==ID_member)
3669  return convert_member(to_member_expr(src), precedence=16);
3670 
3671  else if(src.id()=="array-member-value")
3672  return convert_array_member_value(src, precedence=16);
3673 
3674  else if(src.id()=="struct-member-value")
3675  return convert_struct_member_value(src, precedence=16);
3676 
3677  else if(src.id()==ID_function_application)
3678  return
3680  to_function_application_expr(src), precedence);
3681 
3682  else if(src.id()==ID_side_effect)
3683  {
3684  const irep_idt &statement=src.get(ID_statement);
3685  if(statement==ID_preincrement)
3686  return convert_unary(src, "++", precedence=15);
3687  else if(statement==ID_predecrement)
3688  return convert_unary(src, "--", precedence=15);
3689  else if(statement==ID_postincrement)
3690  return convert_unary_post(src, "++", precedence=16);
3691  else if(statement==ID_postdecrement)
3692  return convert_unary_post(src, "--", precedence=16);
3693  else if(statement==ID_assign_plus)
3694  return convert_binary(src, "+=", precedence=2, true);
3695  else if(statement==ID_assign_minus)
3696  return convert_binary(src, "-=", precedence=2, true);
3697  else if(statement==ID_assign_mult)
3698  return convert_binary(src, "*=", precedence=2, true);
3699  else if(statement==ID_assign_div)
3700  return convert_binary(src, "/=", precedence=2, true);
3701  else if(statement==ID_assign_mod)
3702  return convert_binary(src, "%=", precedence=2, true);
3703  else if(statement==ID_assign_shl)
3704  return convert_binary(src, "<<=", precedence=2, true);
3705  else if(statement==ID_assign_shr)
3706  return convert_binary(src, ">>=", precedence=2, true);
3707  else if(statement==ID_assign_bitand)
3708  return convert_binary(src, "&=", precedence=2, true);
3709  else if(statement==ID_assign_bitxor)
3710  return convert_binary(src, "^=", precedence=2, true);
3711  else if(statement==ID_assign_bitor)
3712  return convert_binary(src, "|=", precedence=2, true);
3713  else if(statement==ID_assign)
3714  return convert_binary(src, "=", precedence=2, true);
3715  else if(statement==ID_function_call)
3716  return
3718  to_side_effect_expr_function_call(src), precedence);
3719  else if(statement == ID_allocate)
3720  return convert_allocate(src, precedence = 15);
3721  else if(statement==ID_printf)
3722  return convert_function(src, "printf", precedence=16);
3723  else if(statement==ID_nondet)
3724  return convert_nondet(src, precedence=16);
3725  else if(statement=="prob_coin")
3726  return convert_prob_coin(src, precedence=16);
3727  else if(statement=="prob_unif")
3728  return convert_prob_uniform(src, precedence=16);
3729  else if(statement==ID_statement_expression)
3730  return convert_statement_expression(src, precedence=15);
3731  else if(statement==ID_gcc_builtin_va_arg_next)
3732  return convert_function(src, "gcc_builtin_va_arg_next", precedence=16);
3733  else
3734  return convert_norep(src, precedence);
3735  }
3736 
3737  else if(src.id()==ID_literal)
3738  return convert_literal(src, precedence=16);
3739 
3740  else if(src.id()==ID_not)
3741  return convert_unary(src, "!", precedence=15);
3742 
3743  else if(src.id()==ID_bitnot)
3744  return convert_unary(src, "~", precedence=15);
3745 
3746  else if(src.id()==ID_mult)
3747  return convert_multi_ary(src, "*", precedence=13, false);
3748 
3749  else if(src.id()==ID_div)
3750  return convert_binary(src, "/", precedence=13, true);
3751 
3752  else if(src.id()==ID_mod)
3753  return convert_binary(src, "%", precedence=13, true);
3754 
3755  else if(src.id()==ID_shl)
3756  return convert_binary(src, "<<", precedence=11, true);
3757 
3758  else if(src.id()==ID_ashr || src.id()==ID_lshr)
3759  return convert_binary(src, ">>", precedence=11, true);
3760 
3761  else if(src.id()==ID_lt || src.id()==ID_gt ||
3762  src.id()==ID_le || src.id()==ID_ge)
3763  return convert_binary(src, src.id_string(), precedence=10, true);
3764 
3765  else if(src.id()==ID_notequal)
3766  return convert_binary(src, "!=", precedence=9, true);
3767 
3768  else if(src.id()==ID_equal)
3769  return convert_binary(src, "==", precedence=9, true);
3770 
3771  else if(src.id()==ID_ieee_float_equal)
3772  return convert_function(src, "IEEE_FLOAT_EQUAL", precedence=16);
3773 
3774  else if(src.id()==ID_width)
3775  return convert_function(src, "WIDTH", precedence=16);
3776 
3777  else if(src.id()==ID_concatenation)
3778  return convert_function(src, "CONCATENATION", precedence=16);
3779 
3780  else if(src.id()==ID_ieee_float_notequal)
3781  return convert_function(src, "IEEE_FLOAT_NOTEQUAL", precedence=16);
3782 
3783  else if(src.id()==ID_abs)
3784  return convert_function(src, "abs", precedence=16);
3785 
3786  else if(src.id()==ID_complex_real)
3787  return convert_function(src, "__real__", precedence=16);
3788 
3789  else if(src.id()==ID_complex_imag)
3790  return convert_function(src, "__imag__", precedence=16);
3791 
3792  else if(src.id()==ID_complex)
3793  return convert_complex(src, precedence=16);
3794 
3795  else if(src.id()==ID_bitand)
3796  return convert_multi_ary(src, "&", precedence=8, false);
3797 
3798  else if(src.id()==ID_bitxor)
3799  return convert_multi_ary(src, "^", precedence=7, false);
3800 
3801  else if(src.id()==ID_bitor)
3802  return convert_multi_ary(src, "|", precedence=6, false);
3803 
3804  else if(src.id()==ID_and)
3805  return convert_multi_ary(src, "&&", precedence=5, false);
3806 
3807  else if(src.id()==ID_or)
3808  return convert_multi_ary(src, "||", precedence=4, false);
3809 
3810  else if(src.id()==ID_xor)
3811  return convert_multi_ary(src, "^", precedence=7, false);
3812 
3813  else if(src.id()==ID_implies)
3814  return convert_binary(src, "==>", precedence=3, true);
3815 
3816  else if(src.id()==ID_if)
3817  return convert_trinary(src, "?", ":", precedence=3);
3818 
3819  else if(src.id()==ID_forall)
3820  return convert_quantifier(src, "forall", precedence=2);
3821 
3822  else if(src.id()==ID_exists)
3823  return convert_quantifier(src, "exists", precedence=2);
3824 
3825  else if(src.id()==ID_lambda)
3826  return convert_quantifier(src, "LAMBDA", precedence=2);
3827 
3828  else if(src.id()==ID_with)
3829  return convert_with(src, precedence=16);
3830 
3831  else if(src.id()==ID_update)
3832  return convert_update(src, precedence=16);
3833 
3834  else if(src.id()==ID_member_designator)
3835  return precedence=16, convert_member_designator(src);
3836 
3837  else if(src.id()==ID_index_designator)
3838  return precedence=16, convert_index_designator(src);
3839 
3840  else if(src.id()==ID_symbol)
3841  return convert_symbol(src, precedence);
3842 
3843  else if(src.id()==ID_next_symbol)
3844  return convert_symbol(src, precedence);
3845 
3846  else if(src.id()==ID_nondet_symbol)
3847  return convert_nondet_symbol(to_nondet_symbol_expr(src), precedence);
3848 
3849  else if(src.id()==ID_predicate_symbol)
3850  return convert_predicate_symbol(src, precedence);
3851 
3852  else if(src.id()==ID_predicate_next_symbol)
3853  return convert_predicate_next_symbol(src, precedence);
3854 
3855  else if(src.id()==ID_predicate_passive_symbol)
3856  return convert_predicate_passive_symbol(src, precedence);
3857 
3858  else if(src.id()=="quant_symbol")
3859  return convert_quantified_symbol(src, precedence);
3860 
3861  else if(src.id()==ID_nondet_bool)
3862  return convert_nondet_bool(src, precedence);
3863 
3864  else if(src.id()==ID_object_descriptor)
3865  return convert_object_descriptor(src, precedence);
3866 
3867  else if(src.id()=="Hoare")
3868  return convert_Hoare(src);
3869 
3870  else if(src.id()==ID_code)
3871  return convert_code(to_code(src));
3872 
3873  else if(src.id()==ID_constant)
3874  return convert_constant(to_constant_expr(src), precedence);
3875 
3876  else if(src.id()==ID_string_constant)
3877  return '"'+MetaString(src.get_string(ID_value))+'"';
3878 
3879  else if(src.id()==ID_struct)
3880  return convert_struct(src, precedence);
3881 
3882  else if(src.id()==ID_vector)
3883  return convert_vector(src, precedence);
3884 
3885  else if(src.id()==ID_union)
3886  return convert_union(src, precedence);
3887 
3888  else if(src.id()==ID_array)
3889  return convert_array(src, precedence);
3890 
3891  else if(src.id() == ID_array_list)
3892  return convert_array_list(src, precedence);
3893 
3894  else if(src.id()==ID_typecast)
3895  return convert_typecast(to_typecast_expr(src), precedence=14);
3896 
3897  else if(src.id()==ID_comma)
3898  return convert_comma(src, precedence=1);
3899 
3900  else if(src.id()==ID_ptr_object)
3901  return "PTR_OBJECT("+id2string(src.get(ID_identifier))+")";
3902 
3903  else if(src.id()==ID_cond)
3904  return convert_cond(src, precedence);
3905 
3906  else if(src.id()==ID_overflow_unary_minus ||
3907  src.id()==ID_overflow_minus ||
3908  src.id()==ID_overflow_mult ||
3909  src.id()==ID_overflow_plus)
3910  return convert_overflow(src, precedence);
3911 
3912  else if(src.id()==ID_unknown)
3913  return "*";
3914 
3915  else if(src.id()==ID_invalid)
3916  return "#";
3917 
3918  else if(src.id()==ID_extractbit)
3919  return convert_extractbit(src, precedence);
3920 
3921  else if(src.id()==ID_extractbits)
3922  return convert_extractbits(src, precedence);
3923 
3924  else if(src.id()==ID_initializer_list ||
3925  src.id()==ID_compound_literal)
3926  return convert_initializer_list(src, precedence=15);
3927 
3928  else if(src.id()==ID_designated_initializer)
3929  return convert_designated_initializer(src, precedence=15);
3930 
3931  else if(src.id()==ID_sizeof)
3932  return convert_sizeof(src, precedence);
3933 
3934  else if(src.id()==ID_let)
3935  return convert_let(to_let_expr(src), precedence=16);
3936 
3937  else if(src.id()==ID_type)
3938  return convert(src.type());
3939 
3940  // no C language expression for internal representation
3941  return convert_norep(src, precedence);
3942 }
3943 
3944 std::string expr2ct::convert(const exprt &src)
3945 {
3946  unsigned precedence;
3947  return convert_with_precedence(src, precedence);
3948 }
3949 
3950 std::string expr2c(const exprt &expr, const namespacet &ns)
3951 {
3952  std::string code;
3953  expr2ct expr2c(ns);
3954  expr2c.get_shorthands(expr);
3955  return expr2c.convert(expr);
3956 }
3957 
3958 std::string type2c(const typet &type, const namespacet &ns)
3959 {
3960  expr2ct expr2c(ns);
3961  // expr2c.get_shorthands(expr);
3962  return expr2c.convert(type);
3963 }
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1204
const irep_idt & get_statement() const
Definition: std_code.h:40
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1474
The type of an expression.
Definition: type.h:22
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3281
const codet & then_case() const
Definition: std_code.h:486
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:1290
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:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
virtual std::string convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
To generate C-like string for defining the given struct.
Definition: expr2c.cpp:659
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:87
application of (mathematical) function
Definition: std_expr.h:4529
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2847
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:1242
exprt & op0()
Definition: expr.h:72
const exprt & cond() const
Definition: std_code.h:617
std::string convert_code_continue(const codet &src, unsigned indent)
Definition: expr2c.cpp:2702
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3130
const exprt & op() const
Definition: std_expr.h:340
const exprt & cond() const
Definition: std_code.h:476
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:3347
const codet & body() const
Definition: std_code.h:766
bool has_ellipsis() const
Definition: std_types.h:861
codet & code()
Definition: std_code.h:1080
const codet & body() const
Definition: std_code.h:690
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2141
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:993
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:1406
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:3312
const irep_idt & get_value() const
Definition: std_expr.h:4439
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:4562
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:2408
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:2809
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3342
bool NULL_is_zero
Definition: config.h:87
std::size_t get_component_number() const
Definition: std_expr.h:3903
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:1341
bitvector_typet double_type()
Definition: c_types.cpp:193
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3047
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:1187
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:1653
A constant literal expression.
Definition: std_expr.h:4422
Structure type.
Definition: std_types.h:297
std::string convert_code_break(const codet &src, unsigned indent)
Definition: expr2c.cpp:2648
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2713
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:2614
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:80
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1711
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:3060
std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence)
Definition: expr2c.cpp:1695
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:4753
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3422
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3108
const exprt & case_op() const
Definition: std_code.h:1070
unsigned sizeof_nesting
Definition: expr2c_class.h:70
Extract member of struct or union.
Definition: std_expr.h:3869
exprt & where()
Definition: std_expr.h:4732
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:1719
std::string convert_code_free(const codet &src, unsigned indent)
Definition: expr2c.cpp:3012
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1766
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:240
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2006
const irep_idt & id() const
Definition: irep.h:259
std::string convert_literal(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1225
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:3001
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3294
argumentst & arguments()
Definition: std_code.h:890
std::string convert_byte_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1376
A reference into the symbol table.
Definition: std_types.h:110
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1735
bitvector_typet float_type()
Definition: c_types.cpp:185
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3160
flavourt mode
Definition: config.h:114
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:1215
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:1010
std::size_t get_fraction_bits() const
Definition: std_types.h:1320
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1536
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:711
A constant-size array type.
Definition: std_types.h:1638
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:648
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3203
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1546
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1489
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:2444
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:4583
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:1648
virtual void read(const typet &src) override
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2302
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2758
A label for branch targets.
Definition: std_code.h:977
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:963
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3034
std::string type2c(const typet &type, const namespacet &ns)
Definition: expr2c.cpp:3958
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
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 struct_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:156
A function call.
Definition: std_code.h:858
#define forall_operands(it, expr)
Definition: expr.h:17
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2268
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:601
size_t size() const
Definition: dstring.h:89
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1232
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1101
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:3405
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
virtual std::string as_string() const override
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3390
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
Definition: expr2c.cpp:2378
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
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:1138
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2094
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:4550
std::vector< exprt > operandst
Definition: expr.h:45
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1703
Pointer Logic.
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1194
bitvector_typet long_double_type()
Definition: c_types.cpp:201
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1642
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3268
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1428
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1622
A function call side effect.
Definition: std_code.h:1395
bool is_extern
Definition: symbol.h:68
std::string convert_byte_extract(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1351
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1526
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:2548
exprt & value()
Definition: std_expr.h:4722
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:1382
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1727
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1343
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3225
exprt & function()
Definition: std_code.h:878
bool is_default() const
Definition: std_code.h:1060
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
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:2772
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:664
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:3436
An inline assembler statement.
Definition: std_code.h:1175
irep_idt get_component_name() const
Definition: std_expr.h:3893
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2832
#define UNREACHABLE
Definition: invariant.h:271
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3247
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:1452
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3950
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
exprt::operandst & arguments()
Definition: std_code.h:1453
const std::string & id_string() const
Definition: irep.h:262
bool is_zero() const
Definition: expr.cpp:161
Sequential composition.
Definition: std_code.h:89
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1632
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
std::string convert_array(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2162
const irep_idt & get_label() const
Definition: std_code.h:1000
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1167
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:787
An if-then-else.
Definition: std_code.h:466
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:1411
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2330
exprt & op2()
Definition: expr.h:78
const char * c_str() const
Definition: dstring.h:84
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
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:1045
symbol_exprt & symbol()
Definition: std_expr.h:4712
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:2636
dstringt irep_idt
Definition: irep.h:32
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:727
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1031
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1266
A let expression.
Definition: std_expr.h:4703
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:2522
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3182
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1742
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:3025
const exprt & cond() const
Definition: std_code.h:680
const codet & else_case() const
Definition: std_code.h:496
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:522
std::vector< c_enum_membert > memberst
Definition: std_types.h:692
bool empty() const
Definition: dstring.h:73
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:627
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition: expr2c.cpp:1997
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:1206
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:2659
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:768
Assignment.
Definition: std_code.h:196
std::size_t short_int_width
Definition: config.h:34
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2439
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2348
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:909
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition: expr2c.cpp:2577
array index operator
Definition: std_expr.h:1462
exprt & op3()
Definition: expr.h:81