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