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