cprover
Loading...
Searching...
No Matches
expr2c.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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>
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
66Precedences are as follows. Higher values mean higher precedence.
67
6816 function call ()
69 ++ -- [] . ->
70
711 comma
72
73*/
74
75irep_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
93static 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)
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 =
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
213std::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=
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=
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,
646 configuration.print_struct_body_in_type,
647 configuration.include_struct_padding_components);
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+=' ';
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)
892 ? ns.follow_tag(to_struct_or_union_tag_type(old.type()))
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
948std::string
949expr2ct::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
1141std::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
1204std::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
1220std::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
1350std::string
1351expr2ct::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
1398std::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
1626std::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
1725static 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
1796 if(!configuration.print_enum_int_value)
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 =
1812
1813 std::string value_as_string =
1814 integer2string(bvrep2integer(value, width, is_signed));
1815
1816 if(configuration.print_enum_int_value)
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 {
1907 dest = convert(sizeof_expr_opt.value()) + " /*" + dest + "*/ ";
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 {
1932 if(configuration.use_library_macros)
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 {
1987 if(configuration.use_library_macros)
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
2030std::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(
2043 src, precedence, configuration.include_struct_padding_components);
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
2064 ? ns.follow_tag(to_struct_tag_type(src.type()))
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
2193std::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
2356std::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 }
2374 {
2375 // Set the type width
2376 type_width = to_unsignedbv_type(op0.type()).get_width();
2377 }
2378 else
2379 {
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.
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
2458std::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
2547std::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
2755std::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
2807std::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
2816std::string
2817expr2ct::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(
2840 symbol->is_exported && config.ansi_c.os == configt::ansi_ct::ost::OS_WIN)
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();
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
3433std::string expr2ct::convert_code(const codet &src)
3434{
3435 return convert_code(src, 0);
3436}
3437
3438std::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
3481std::string
3482expr2ct::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
3492std::string
3493expr2ct::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
3587std::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)
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;
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)
4055
4056 else if(
4057 auto prophecy_r_or_w_ok =
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
4080std::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
4137std::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
4155std::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
4166std::string expr2c(const exprt &expr, const namespacet &ns)
4167{
4169}
4170
4171std::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
4181std::string type2c(const typet &type, const namespacet &ns)
4182{
4184}
4185
4186std::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))
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_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
unsignedbv_typet size_type()
Definition c_types.cpp:50
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_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 c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
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
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
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 & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:3112
exprt & where()
Definition std_expr.h:3143
variablest & variables()
Definition std_expr.h:3133
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
const typet & underlying_type() const
Definition c_types.h:307
memberst & members()
Definition c_types.h:283
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 codet & body() const
Definition std_code.h:689
const exprt & cond() const
Definition std_code.h:679
codet representation of a for statement.
Definition std_code.h:734
const exprt & cond() const
Definition std_code.h:759
const exprt & iter() const
Definition std_code.h:769
const codet & body() const
Definition std_code.h:779
const exprt & init() const
Definition std_code.h:749
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 exprt & cond() const
Definition std_code.h:478
const codet & else_case() const
Definition std_code.h:498
const codet & then_case() const
Definition std_code.h:488
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
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:586
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
bool has_ellipsis() const
Definition std_types.h:655
codet representing a while statement.
Definition std_code.h:610
const exprt & cond() const
Definition std_code.h:617
const codet & body() const
Definition std_code.h:627
Data structure for representing an arbitrary statement in a program.
exprt & op3()
Definition expr.h:142
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
const irep_idt & get_statement() const
A constant literal expression.
Definition std_expr.h:2995
const irep_idt & get_value() const
Definition std_expr.h:3003
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
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
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
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
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
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
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
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
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
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
bool is_not_nil() const
Definition irep.h:372
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
A let expression.
Definition std_expr.h:3209
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3290
operandst & values()
Definition std_expr.h:3279
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3302
std::string expr2string() const
Definition lispexpr.cpp:15
Extract member of struct or union.
Definition std_expr.h:2849
const exprt & compound() const
Definition std_expr.h:2898
irep_idt get_component_name() const
Definition std_expr.h:2871
std::size_t get_component_number() const
Definition std_expr.h:2881
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
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)) ∧...
const exprt & upper_bound() const
const exprt & lower_bound() const
const exprt & pointer() const
const typet & base_type() const
The type of the data what we point to.
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
const exprt & upper_bound() const
const exprt & lower_bound() 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.
const exprt & pointer() const
const exprt & size() const
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 shift and rotate operators.
exprt & distance()
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 irept::named_subt & get_pragmas() const
const irep_idt & get_comment() 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 componentst & components() const
Definition std_types.h:147
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
std::vector< componentt > componentst
Definition std_types.h:140
Expression to hold a symbol (variable)
Definition std_expr.h:131
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 & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
const typet & subtype() const
Definition type.h:187
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
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:2660
The vector type.
Definition std_types.h:1061
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1077
exprt & old()
Definition std_expr.h:2486
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
static std::unordered_set< irep_idt > find_symbol_identifiers(const goto_programt &src)
Find all identifiers in src.
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
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition expr_cast.h:242
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
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.
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
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_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)
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)
const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const code_switch_caset & to_code_switch_case(const codet &code)
Definition std_code.h:1077
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition std_code.h:943
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_whilet & to_code_while(const codet &code)
Definition std_code.h:654
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition std_code.h:530
const code_frontend_assignt & to_code_frontend_assign(const codet &code)
Definition std_code.h:113
code_asmt & to_code_asm(codet &code)
Definition std_code.h:1282
const code_fort & to_code_for(const codet &code)
Definition std_code.h:823
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 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:1538
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1277
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1206
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1450
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
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 let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3333
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2455
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2941
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1816
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3050
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2357
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2538
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2213
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2743
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1113
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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
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 complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1155
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
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 string_constantt & to_string_constant(const exprt &expr)
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.
Used for configuring the behaviour of expr2c and type2c.
Definition expr2c.h:21
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition expr2c.h:52
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:40
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
Symbol table entry.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45
dstringt irep_idt