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