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