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 }
MetaString
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
c_qualifierst::read
virtual void read(const typet &src) override
Definition: c_qualifiers.cpp:62
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
irep2lisp
void irep2lisp(const irept &src, lispexprt &dest)
Definition: lispirep.cpp:43
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:563
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_c_enum_tag_type
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
code_switch_caset::case_op
const exprt & case_op() const
Definition: std_code.h:1488
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:215
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:71
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:816
ieee_floatt
Definition: ieee_float.h:120
expr2ct::convert_code_while
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition: expr2c.cpp:2491
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2422
dstringt::c_str
const char * c_str() const
Definition: dstring.h:99
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:411
expr2ct::convert_prob_uniform
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1177
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:168
typet::subtype
const typet & subtype() const
Definition: type.h:47
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1471
expr2ct::convert_code_fence
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3082
c_enum_typet
The type of C enums.
Definition: std_types.h:628
extractbits_exprt::lower
exprt & lower()
Definition: bitvector_expr.h:461
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2187
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1030
expr2ct::convert_cond
std::string convert_cond(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:955
can_cast_expr< code_inputt >
bool can_cast_expr< code_inputt >(const exprt &base)
Definition: std_code.h:705
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
code_fort::cond
const exprt & cond() const
Definition: std_code.h:1077
arith_tools.h
code_whilet
codet representing a while statement.
Definition: std_code.h:928
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:210
codet::op0
exprt & op0()
Definition: expr.h:103
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:67
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:209
expr2ct::convert_union
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2097
expr2c_configurationt::print_enum_int_value
bool print_enum_int_value
When printing an enum-typed constant, print the integer representation.
Definition: expr2c.h:43
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1701
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
code_fort
codet representation of a for statement.
Definition: std_code.h:1052
nondet_symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:238
pos
literalt pos(literalt a)
Definition: literal.h:194
expr2ct::convert_statement_expression
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1147
ternary_exprt::op2
exprt & op2()
Definition: expr.h:109
string_utils.h
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:689
typet
The type of an expression, extends irept.
Definition: type.h:28
source_locationt::get_pragmas
const irept::named_subt & get_pragmas() const
Definition: source_location.h:200
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
clean_identifier
static std::string clean_identifier(const irep_idt &id)
Definition: expr2c.cpp:95
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:806
ternary_exprt
An expression with three operands.
Definition: std_expr.h:54
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
expr2ct::convert_comma
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1209
expr2ct::convert_pointer_arithmetic
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1390
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
expr2c_configurationt::use_library_macros
bool use_library_macros
This is the string that will be printed for null pointers.
Definition: expr2c.h:40
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
expr2ct::convert_code_assert
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3220
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
expr2ct::convert_with_identifier
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
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
long_double_type
floatbv_typet long_double_type()
Definition: c_types.cpp:201
ieee_floatt::to_ansi_c_string
std::string to_ansi_c_string() const
Definition: ieee_float.h:269
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
find_symbol_identifiers
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
Definition: find_symbols.cpp:81
expr2ct::convert_quantifier
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:804
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
configt::ansi_ct::os
ost os
Definition: config.h:160
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: std_types.h:652
is_signed
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
pointer_predicates.h
Various predicates over pointers in programs.
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
expr2ct::convert_code_function_call
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2c.cpp:3012
expr2ct::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1693
expr2ct::convert_update
std::string convert_update(const update_exprt &, unsigned precedence)
Definition: expr2c.cpp:917
expr2ct::convert_let
std::string convert_let(const let_exprt &, unsigned precedence)
Definition: expr2c.cpp:896
expr2ct::convert_byte_extract
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
Definition: expr2c.cpp:1293
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
expr2ct::convert_code_decl
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2677
fixedbv.h
let_exprt::symbol
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:2855
expr2ct::convert_code_decl_block
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2796
expr2ct::convert_nondet_bool
std::string convert_nondet_bool()
Definition: expr2c.cpp:1664
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
ternary_exprt::op1
exprt & op1()
Definition: expr.h:106
expr2ct::convert_code_expression
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2811
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
code_fort::iter
const exprt & iter() const
Definition: std_code.h:1087
expr2ct::convert_quantified_symbol
std::string convert_quantified_symbol(const exprt &src)
Definition: expr2c.cpp:1658
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:282
expr2ct::convert_array_list
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2217
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1563
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:498
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:33
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
expr2c_configurationt::default_configuration
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
to_code_while
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:972
irep_idt
dstringt irep_idt
Definition: irep.h:37
vector_typet
The vector type.
Definition: std_types.h:1764
struct_union_typet::componentt::get_pretty_name
const irep_idt & get_pretty_name() const
Definition: std_types.h:104
expr2ct::convert_code_input
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3112
quantifier_exprt
A base class for quantifier expressions.
Definition: mathematical_expr.h:265
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:796
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: bitvector_expr.h:106
expr2ct::convert_Hoare
std::string convert_Hoare(const exprt &src)
Definition: expr2c.cpp:3300
expr2ct::convert_code
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3295
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
expr2ct::convert_constant_bool
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition: expr2c.cpp:1953
c_qualifiers.h
expr2ct::convert_array_of
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1283
expr2ct::convert_unary_post
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1344
configt::ansi_c
struct configt::ansi_ct ansi_c
expr2ct::convert_code_ifthenelse
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition: expr2c.cpp:2546
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
qualifierst
Definition: c_qualifiers.h:19
namespace.h
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
expr2ct::convert_struct_type
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
expr2ct::convert_code_switch_case
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition: expr2c.cpp:3265
expr2ct::convert_predicate_symbol
std::string convert_predicate_symbol(const exprt &src)
Definition: expr2c.cpp:1640
to_code_for
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:1141
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
expr2ct::shorthands
std::unordered_map< irep_idt, irep_idt > shorthands
Definition: expr2c_class.h:83
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:778
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:538
code_labelt::code
codet & code()
Definition: std_code.h:1425
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
expr2ct::convert_trinary
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
Definition: expr2c.cpp:757
extractbits_exprt::upper
exprt & upper()
Definition: bitvector_expr.h:456
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
expr2ct::convert_code_assign
std::string convert_code_assign(const code_assignt &src, unsigned indent)
Definition: expr2c.cpp:2978
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
lispexpr.h
expr2ct::sizeof_nesting
unsigned sizeof_nesting
Definition: expr2c_class.h:85
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:114
to_code_switch_case
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1525
expr2ct::convert_overflow
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2377
expr2ct::ns_collision
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:82
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
to_nondet_symbol_expr
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:261
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
let_exprt::value
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:2871
expr2ct::convert_typecast
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:723
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
expr2ct::convert_predicate_passive_symbol
std::string convert_predicate_passive_symbol(const exprt &src)
Definition: expr2c.cpp:1652
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
expr2ct
Definition: expr2c_class.h:29
member_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:2552
with_exprt::old
exprt & old()
Definition: std_expr.h:2183
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:163
expr2ct::convert
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:187
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:990
expr2ct::convert_code_array_set
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3155
expr2ct::convert_code_for
std::string convert_code_for(const code_fort &src, unsigned indent)
Definition: expr2c.cpp:2736
expr2ct::convert_member_designator
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1466
expr2ct::convert_array_member_value
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1560
find_symbols.h
code_fort::init
const exprt & init() const
Definition: std_code.h:1067
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1369
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
code_switch_caset::is_default
bool is_default() const
Definition: std_code.h:1478
expr2ct::convert_nondet_symbol
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
Definition: expr2c.cpp:1634
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1075
expr2ct::convert_code_printf
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3060
lispexprt::expr2string
std::string expr2string() const
Definition: lispexpr.cpp:15
lispirep.h
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
expr2ct::indent_str
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2408
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:119
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2569
fixedbvt::to_ansi_c_string
std::string to_ansi_c_string() const
Definition: fixedbv.h:62
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:120
SYMEX_DYNAMIC_PREFIX
#define SYMEX_DYNAMIC_PREFIX
Definition: pointer_predicates.h:17
expr2ct::convert_function
std::string convert_function(const exprt &src, const std::string &symbol)
Definition: expr2c.cpp:1188
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3921
join_strings
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
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:848
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
quantifier_exprt::symbol
symbol_exprt & symbol()
Definition: mathematical_expr.h:280
qualifierst::clone
virtual std::unique_ptr< qualifierst > clone() const =0
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
ternary_exprt::op0
exprt & op0()
Definition: expr.h:103
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:269
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
expr2ct::convert_pointer_difference
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1427
wchar_t_type
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
expr2ct::convert_prob_coin
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1162
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1452
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2940
to_c_bit_field_type
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
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:870
pointer_expr.h
API to expression classes for Pointers.
expr2c_configurationt::include_struct_padding_components
bool include_struct_padding_components
When printing struct_typet or struct_exprt, include the artificial padding components introduced to k...
Definition: expr2c.h:24
c_misc.h
ANSI-C Misc Utilities.
expr2ct::convert_code_asm
std::string convert_code_asm(const code_asmt &src, unsigned indent)
Definition: expr2c.cpp:2413
extractbits_exprt::src
exprt & src()
Definition: bitvector_expr.h:451
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:194
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1223
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:116
c_qualifierst
Definition: c_qualifiers.h:61
symbolt::is_exported
bool is_exported
Definition: symbol.h:61
to_code_dowhile
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:1034
expr2ct::convert_code_lock
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:2986
expr2ct::convert_code_label
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3247
expr2ct::convert_unary
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1090
expr2ct::convert_extractbits
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
Definition: expr2c.cpp:3355
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
expr2ct::convert_array
std::string convert_array(const exprt &src)
Definition: expr2c.cpp:2116
extractbit_exprt::index
exprt & index()
Definition: bitvector_expr.h:378
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
expr2c_class.h
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:935
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
symbol.h
Symbol table entry.
expr2ct::convert_code_goto
std::string convert_code_goto(const codet &src, unsigned indent)
Definition: expr2c.cpp:2604
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
expr2ct::convert_symbol
virtual std::string convert_symbol(const exprt &src)
Definition: expr2c.cpp:1591
code_whilet::body
const codet & body() const
Definition: std_code.h:945
irept::is_nil
bool is_nil() const
Definition: irep.h:387
codet::op2
exprt & op2()
Definition: expr.h:109
irept::id
const irep_idt & id() const
Definition: irep.h:407
expr2ct::convert_predicate_next_symbol
std::string convert_predicate_next_symbol(const exprt &src)
Definition: expr2c.cpp:1646
expr2ct::convert_index
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1366
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
expr2ct::convert_byte_update
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
Definition: expr2c.cpp:1319
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
expr2ct::convert_code_assume
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3233
dstringt::empty
bool empty() const
Definition: dstring.h:88
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1391
floatbv_expr.h
API to expression classes for floating-point arithmetic.
union_typet
The union type.
Definition: std_types.h:393
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
expr2ct::convert_struct
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1961
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: bitvector_expr.h:314
expr2ct::convert_initializer_list
std::string convert_initializer_list(const exprt &src)
Definition: expr2c.cpp:2251
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
cprover_prefix.h
expr2ct::convert_side_effect_expr_function_call
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
Definition: expr2c.cpp:2348
expr2ct::configuration
const expr2c_configurationt & configuration
Definition: expr2c_class.h:50
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:282
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: bitvector_expr.h:278
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
expr2ct::convert_code_continue
std::string convert_code_continue(unsigned indent)
Definition: expr2c.cpp:2668
expr2ct::convert_code_break
std::string convert_code_break(unsigned indent)
Definition: expr2c.cpp:2616
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
config
configt config
Definition: config.cpp:24
expr2ct::convert_code_array_copy
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3177
expr2ct::convert_extractbit
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
Definition: expr2c.cpp:3344
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1048
code_labelt::get_label
const irep_idt & get_label() const
Definition: std_code.h:1415
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
expr2ct::convert_norep
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1580
expr2ct::convert_literal
std::string convert_literal(const exprt &src)
Definition: expr2c.cpp:1172
to_code_asm
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1730
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2528
struct_union_typet::componentt
Definition: std_types.h:64
lispexprt
Definition: lispexpr.h:74
expr2ct::ns
const namespacet & ns
Definition: expr2c_class.h:49
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
configt::ansi_ct::mode
flavourt mode
Definition: config.h:196
expr2ct::convert_function_application
std::string convert_function_application(const function_application_exprt &src)
Definition: expr2c.cpp:2320
expr2ct::convert_with
std::string convert_with(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:827
can_cast_expr< code_outputt >
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:751
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:704
expr2ct::convert_code_block
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition: expr2c.cpp:2773
c_type_as_string
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:259
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
build_sizeof_expr
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:562
binding_exprt::where
exprt & where()
Definition: std_expr.h:2803
fixedbv_typet::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: std_types.h:1331
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:316
expr2ct::convert_code_array_replace
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3199
suffix.h
expr2c_configurationt::print_struct_body_in_type
bool print_struct_body_in_type
When printing a struct_typet, should the components of the struct be printed inline.
Definition: expr2c.h:28
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
expr2ct::convert_code_unlock
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:2999
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:202
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:1923
expr2ct::convert_nondet
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1137
expr2ct::get_shorthands
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:118
symbolt
Symbol table entry.
Definition: symbol.h:28
code_dowhilet::body
const codet & body() const
Definition: std_code.h:1007
extractbit_exprt::src
exprt & src()
Definition: bitvector_expr.h:373
expr2ct::convert_code_dowhile
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition: expr2c.cpp:2517
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:2166
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
code_fort::body
const codet & body() const
Definition: std_code.h:1097
expr2ct::convert_object_descriptor
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1669
code_ifthenelset::else_case
const codet & else_case() const
Definition: std_code.h:816
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:120
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
expr2ct::convert_sizeof
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3367
expr2ct::convert_array_type
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
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1180
codet::op3
exprt & op3()
Definition: expr.h:112
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
code_switch_caset::code
codet & code()
Definition: std_code.h:1498
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:870
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:115
expr2ct::id_shorthand
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:77
code_dowhilet::cond
const exprt & cond() const
Definition: std_code.h:997
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:124
fixedbvt
Definition: fixedbv.h:42
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: bitvector_expr.h:499
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1789
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
expr2c_configurationt::clean_configuration
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition: expr2c.h:75
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2542
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
expr2ct::convert_code_dead
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2722
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
side_effect_expr_function_callt::function
exprt & function()
Definition: std_code.h:2156
exprt::operands
operandst & operands()
Definition: expr.h:96
expr2c_configurationt::include_array_size
bool include_array_size
When printing array_typet, should the size of the array be printed.
Definition: expr2c.h:31
type2c
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3937
expr2ct::convert_struct_member_value
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1570
codet::op1
exprt & op1()
Definition: expr.h:106
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:30
index_exprt
Array index operator.
Definition: std_expr.h:1243
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:118
expr2ct::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:192
expr2ct::convert_index_designator
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1476
expr2c_configurationt
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:21
code_asmt::get_flavor
const irep_idt & get_flavor() const
Definition: std_code.h:1711
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
expr2ct::convert_code_switch
std::string convert_code_switch(const codet &src, unsigned indent)
Definition: expr2c.cpp:2625
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
expr2ct::convert_member
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1486
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
expr2c_configurationt::true_string
std::string true_string
This is the string that will be printed for the true boolean expression.
Definition: expr2c.h:34
expr2ct::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3381
c_qualifierst::as_string
virtual std::string as_string() const override
Definition: c_qualifiers.cpp:34
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
c_qualifierst::is_noreturn
bool is_noreturn
Definition: c_qualifiers.h:91
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:2909
expr2ct::convert_multi_ary
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1041
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
struct_union_typet::is_incomplete
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:180
expr2ct::convert_complex
std::string convert_complex(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1233
expr2ct::convert_code_output
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3134
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:111
c_types.h
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:244
expr2c_configurationt::expand_typedef
bool expand_typedef
Print the expanded type instead of a typedef name, even when a typedef is present.
Definition: expr2c.h:47
expr2ct::convert_designated_initializer
std::string convert_designated_initializer(const exprt &src)
Definition: expr2c.cpp:2277
expr2ct::convert_vector
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2050
expr2ct::convert_binary
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:989
expr2c_configurationt::false_string
std::string false_string
This is the string that will be printed for the false boolean expression.
Definition: expr2c.h:37
let_exprt
A let expression.
Definition: std_expr.h:2816
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
dstringt::size
size_t size() const
Definition: dstring.h:104
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:112
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
c_enum_typet::members
const memberst & members() const
Definition: std_types.h:654
expr2ct::convert_allocate
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1110
expr2ct::convert_code_return
std::string convert_code_return(const codet &src, unsigned indent)
Definition: expr2c.cpp:2583
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106