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