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