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