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