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