cprover
Loading...
Searching...
No Matches
string_abstraction.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String Abstraction
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "string_abstraction.h"
13
14#include <algorithm>
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/expr_util.h>
19#include <util/fresh_symbol.h>
20#include <util/message.h>
21#include <util/pointer_expr.h>
23#include <util/std_code.h>
25
26#include "goto_model.h"
27#include "pointer_arithmetic.h"
28
30 const exprt &object,
31 exprt &dest, bool write)
32{
33 // debugging
34 if(build(object, dest, write))
35 return true;
36
37 // extra consistency check
38 // use
39 // #define build_wrap(a,b,c) build(a,b,c)
40 // to avoid it
41 const typet &a_t=build_abstraction_type(object.type());
42 /*assert(dest.type() == a_t ||
43 (dest.type().id()==ID_array && a_t.id()==ID_pointer &&
44 dest.type().subtype() == a_t.subtype()));
45 */
46 if(
47 dest.type() != a_t &&
48 !(dest.type().id() == ID_array && a_t.id() == ID_pointer &&
49 dest.type().subtype() == a_t.subtype()))
50 {
52 log.warning() << "warning: inconsistent abstract type for "
53 << object.pretty() << messaget::eom;
54 return true;
55 }
56
57 return false;
58}
59
61{
62 return type.id() == ID_pointer && type.subtype() == string_struct;
63}
64
65static inline bool is_ptr_argument(const typet &type)
66{
67 return type.id()==ID_pointer;
68}
69
71 symbol_tablet &symbol_table,
72 message_handlert &message_handler,
74{
75 string_abstractiont string_abstraction(symbol_table, message_handler);
77}
78
80 goto_modelt &goto_model,
81 message_handlert &message_handler)
82{
83 string_abstractiont{goto_model.symbol_table, message_handler}.apply(
84 goto_model);
85}
86
90 : sym_suffix("#str$fcn"),
91 symbol_table(_symbol_table),
92 ns(_symbol_table),
93 temporary_counter(0),
94 message_handler(_message_handler)
95{
96 struct_typet s({{"is_zero", build_type(whatt::IS_ZERO)},
97 {"length", build_type(whatt::LENGTH)},
98 {"size", build_type(whatt::SIZE)}});
99 s.components()[0].set_pretty_name("is_zero");
100 s.components()[1].set_pretty_name("length");
101 s.components()[2].set_pretty_name("size");
102
104 s, "tag-", "string_struct", source_locationt{}, ID_C, ns, symbol_table);
105 struct_symbol.is_type = true;
106 struct_symbol.is_lvalue = false;
107 struct_symbol.is_state_var = false;
108 struct_symbol.is_thread_local = true;
109 struct_symbol.is_file_local = true;
110 struct_symbol.is_auxiliary = false;
111 struct_symbol.is_macro = true;
112
114}
115
117{
118 typet type;
119
120 // clang-format off
121 switch(what)
122 {
123 case whatt::IS_ZERO: type=c_bool_type(); break;
124 case whatt::LENGTH: type=size_type(); break;
125 case whatt::SIZE: type=size_type(); break;
126 }
127 // clang-format on
128
129 return type;
130}
131
133{
134 operator()(goto_model.goto_functions);
135}
136
138{
139 // iterate over all previously known symbols as the body of the loop modifies
140 // the symbol table and can thus invalidate iterators
142 {
144
145 if(type.id() != ID_code)
146 continue;
147
148 sym_suffix = "#str$" + id2string(sym_name);
149
150 goto_functionst::function_mapt::iterator fct_entry =
151 dest.function_map.find(sym_name);
152 if(fct_entry != dest.function_map.end())
153 {
156 fct_entry->second.parameter_identifiers);
157 }
158 else
159 {
161 to_code_type(type).parameters().size(), irep_idt{});
163 }
164 }
165
166 for(auto &gf_entry : dest.function_map)
167 {
168 sym_suffix = "#str$" + id2string(gf_entry.first);
169 abstract(gf_entry.second.body);
170 }
171
172 // do we have a main?
173 goto_functionst::function_mapt::iterator
174 m_it=dest.function_map.find(dest.entry_point());
175
176 if(m_it!=dest.function_map.end())
177 {
178 goto_programt &main=m_it->second.body;
179
180 // do initialization
182 main.swap(initialization);
184 }
185}
186
196
199 goto_functiont::parameter_identifierst &parameter_identifiers)
200{
202 PRECONDITION(fct_type.parameters().size() == parameter_identifiers.size());
203
205
206 goto_functiont::parameter_identifierst::const_iterator param_id_it =
207 parameter_identifiers.begin();
208 for(const auto &parameter : fct_type.parameters())
209 {
211 if(abstract_type.is_nil())
212 continue;
213
215 ++param_id_it;
216 }
217
218 for(const auto &new_param : str_args)
219 parameter_identifiers.push_back(new_param.get_identifier());
220 fct_type.parameters().insert(
221 fct_type.parameters().end(), str_args.begin(), str_args.end());
222}
223
225 const symbolt &fct_symbol,
226 const typet &type,
227 const irep_idt &identifier)
228{
229 typet final_type=is_ptr_argument(type)?
230 type:pointer_type(type);
231
233 final_type,
234 id2string(identifier.empty() ? fct_symbol.name : identifier),
235 id2string(
236 identifier.empty() ? fct_symbol.base_name
237 : ns.lookup(identifier).base_name) +
238 "#str",
239 fct_symbol.location,
240 fct_symbol.mode,
242 param_symbol.is_parameter = true;
243 param_symbol.value.make_nil();
244
246 str_parameter.add_source_location() = fct_symbol.location;
247 str_parameter.set_base_name(param_symbol.base_name);
248 str_parameter.set_identifier(param_symbol.name);
249
250 if(!identifier.empty())
251 parameter_map.insert(std::make_pair(identifier, param_symbol.name));
252
253 return str_parameter;
254}
255
257{
258 locals.clear();
259
261 it=abstract(dest, it);
262
263 if(locals.empty())
264 return;
265
266 // go over it again for the newly added locals
268 locals.clear();
269}
270
272{
273 typedef std::unordered_map<irep_idt, goto_programt::targett> available_declst;
275
277 if(it->is_decl())
278 // same name may exist several times due to inlining, make sure the first
279 // declaration is used
280 available_decls.insert(
281 std::make_pair(it->decl_symbol().get_identifier(), it));
282
283 // declare (and, if necessary, define) locals
284 for(const auto &l : locals)
285 {
286 goto_programt::targett ref_instr=dest.instructions.begin();
287 bool has_decl=false;
288
289 available_declst::const_iterator entry=available_decls.find(l.first);
290
291 if(available_declst::const_iterator(available_decls.end())!=entry)
292 {
293 ref_instr=entry->second;
294 has_decl=true;
295 }
296
298 make_decl_and_def(tmp, ref_instr, l.second, l.first);
299
300 if(has_decl)
301 ++ref_instr;
302 dest.insert_before_swap(ref_instr, tmp);
303 }
304}
305
308 const irep_idt &identifier,
309 const irep_idt &source_sym)
310{
311 const symbolt &symbol=ns.lookup(identifier);
313
315 dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location()));
316 decl1->code_nonconst().add_source_location() = ref_instr->source_location();
317
318 exprt val=symbol.value;
319 // initialize pointers with suitable objects
320 if(val.is_nil())
321 {
323 val = make_val_or_dummy_rec(dest, ref_instr, symbol, orig.type);
324 }
325
326 // may still be nil (structs, then assignments have been done already)
327 if(val.is_not_nil())
328 {
331 code_assignt(sym_expr, val), ref_instr->source_location()));
332 assignment1->code_nonconst().add_source_location() =
333 ref_instr->source_location();
334 }
335}
336
339 const symbolt &symbol, const typet &source_type)
340{
341 if(symbol.type.id() == ID_array || symbol.type.id() == ID_pointer)
342 {
343 const typet &source_subt =
344 is_ptr_string_struct(symbol.type) ? source_type : source_type.subtype();
346 dest, ref_instr, symbol, irep_idt(), symbol.type.subtype(), source_subt);
347
348 if(symbol.type.id() == ID_array)
349 return array_of_exprt(sym_expr, to_array_type(symbol.type));
350 else
352 }
353 else if(
354 symbol.type.id() == ID_union_tag ||
355 (symbol.type.id() == ID_struct_tag && symbol.type != string_struct))
356 {
360 su_source.components();
363 const struct_union_typet::componentst &components=
364 struct_union_type.components();
365 unsigned seen=0;
366
367 struct_union_typet::componentst::const_iterator it2=components.begin();
368 for(struct_union_typet::componentst::const_iterator
369 it=s_components.begin();
370 it!=s_components.end() && it2!=components.end();
371 ++it)
372 {
373 if(it->get_name()!=it2->get_name())
374 continue;
375
376 if(
377 it2->type().id() == ID_pointer || it2->type().id() == ID_array ||
378 it2->type().id() == ID_struct_tag || it2->type().id() == ID_union_tag)
379 {
381 dest, ref_instr, symbol, it2->get_name(), it2->type(), it->type());
382
383 member_exprt member(symbol.symbol_expr(), it2->get_name(), it2->type());
384
387 code_assignt(member, sym_expr), ref_instr->source_location()));
388 assignment1->code_nonconst().add_source_location() =
389 ref_instr->source_location();
390 }
391
392 ++seen;
393 ++it2;
394 }
395
396 INVARIANT(
397 components.size() == seen,
398 "some of the symbol's component names were not found in the source");
399 }
400
401 return nil_exprt();
402}
403
407 const symbolt &symbol,
408 const irep_idt &component_name,
409 const typet &type,
410 const typet &source_type)
411{
412 std::string suffix="$strdummy";
413 if(!component_name.empty())
414 suffix="#"+id2string(component_name)+suffix;
415
417
418 auxiliary_symbolt new_symbol;
419 new_symbol.type=type;
420 new_symbol.value.make_nil();
421 new_symbol.location = ref_instr->source_location();
422 new_symbol.name=dummy_identifier;
423 new_symbol.module=symbol.module;
424 new_symbol.base_name=id2string(symbol.base_name)+suffix;
425 new_symbol.mode=symbol.mode;
426 new_symbol.pretty_name=id2string(
427 symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+suffix;
428
429 symbol_exprt sym_expr=new_symbol.symbol_expr();
430
431 // make sure it is declared before the recursive call
433 dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location()));
434 decl->code_nonconst().add_source_location() = ref_instr->source_location();
435
436 // set the value - may be nil
437 if(
438 source_type.id() == ID_array && is_char_type(source_type.subtype()) &&
439 type == string_struct)
440 {
441 new_symbol.value = struct_exprt(
445 ? build_unknown(whatt::SIZE, false)
448
450 }
451 else
452 new_symbol.value=
454
455 if(new_symbol.value.is_not_nil())
456 {
459 code_assignt(sym_expr, new_symbol.value),
460 ref_instr->source_location()));
461 assignment1->code_nonconst().add_source_location() =
462 ref_instr->source_location();
463 }
464
465 symbol_table.insert(std::move(new_symbol));
466
467 return sym_expr;
468}
469
473{
474 switch(it->type())
475 {
476 case ASSIGN:
477 it=abstract_assign(dest, it);
478 break;
479
480 case GOTO:
481 case ASSERT:
482 case ASSUME:
483 if(has_string_macros(it->get_condition()))
484 {
485 exprt tmp = it->get_condition();
486 replace_string_macros(tmp, false, it->source_location());
487 it->set_condition(tmp);
488 }
489 break;
490
491 case FUNCTION_CALL:
493 break;
494
495 case SET_RETURN_VALUE:
496 // use remove_returns
498 break;
499
500 case END_FUNCTION:
501 case START_THREAD:
502 case END_THREAD:
503 case ATOMIC_BEGIN:
504 case ATOMIC_END:
505 case DECL:
506 case DEAD:
507 case CATCH:
508 case THROW:
509 case SKIP:
510 case OTHER:
511 case LOCATION:
512 break;
513
514 case INCOMPLETE_GOTO:
517 break;
518 }
519
520 return it;
521}
522
526{
527 {
528 exprt &lhs = target->assign_lhs_nonconst();
529 exprt &rhs = target->assign_rhs_nonconst();
530
531 if(has_string_macros(lhs))
532 {
533 replace_string_macros(lhs, true, target->source_location());
534 move_lhs_arithmetic(lhs, rhs);
535 }
536
537 if(has_string_macros(rhs))
538 replace_string_macros(rhs, false, target->source_location());
539 }
540
541 const typet &type = target->assign_lhs().type();
542
543 if(type.id() == ID_pointer || type.id() == ID_array)
544 return abstract_pointer_assign(dest, target);
545 else if(is_char_type(type))
546 return abstract_char_assign(dest, target);
547
548 return target;
549}
550
553{
554 auto arguments = as_const(*target).call_arguments();
556
557 for(const auto &arg : arguments)
558 {
559 const typet &abstract_type = build_abstraction_type(arg.type());
560 if(abstract_type.is_nil())
561 continue;
562
563 str_args.push_back(exprt());
564 // if function takes void*, build for `arg` will fail if actual parameter
565 // is of some other pointer type; then just introduce an unknown
566 if(build_wrap(arg, str_args.back(), false))
567 str_args.back()=build_unknown(abstract_type, false);
568 // array -> pointer translation
569 if(str_args.back().type().id()==ID_array &&
571 {
572 INVARIANT(
573 str_args.back().type().subtype() == abstract_type.subtype(),
574 "argument array type differs from formal parameter pointer type");
575
577 // disable bounds check on that one
578 idx.set(ID_C_bounds_check, false);
579
580 str_args.back()=address_of_exprt(idx);
581 }
582
584 str_args.back()=address_of_exprt(str_args.back());
585 }
586
587 if(!str_args.empty())
588 {
589 arguments.insert(arguments.end(), str_args.begin(), str_args.end());
590
591 auto &parameters =
592 to_code_type(target->call_function().type()).parameters();
593 for(const auto &arg : str_args)
594 parameters.push_back(code_typet::parametert{arg.type()});
595
596 target->call_arguments() = std::move(arguments);
597 }
598}
599
601{
602 if(expr.id()=="is_zero_string" ||
603 expr.id()=="zero_string_length" ||
604 expr.id()=="buffer_size")
605 return true;
606
607 forall_operands(it, expr)
608 if(has_string_macros(*it))
609 return true;
610
611 return false;
612}
613
615 exprt &expr,
616 bool lhs,
617 const source_locationt &source_location)
618{
619 if(expr.id()=="is_zero_string")
620 {
621 PRECONDITION(expr.operands().size() == 1);
622 exprt tmp =
623 build(to_unary_expr(expr).op(), whatt::IS_ZERO, lhs, source_location);
624 expr.swap(tmp);
625 }
626 else if(expr.id()=="zero_string_length")
627 {
628 PRECONDITION(expr.operands().size() == 1);
629 exprt tmp =
630 build(to_unary_expr(expr).op(), whatt::LENGTH, lhs, source_location);
631 expr.swap(tmp);
632 }
633 else if(expr.id()=="buffer_size")
634 {
635 PRECONDITION(expr.operands().size() == 1);
636 exprt tmp =
637 build(to_unary_expr(expr).op(), whatt::SIZE, false, source_location);
638 expr.swap(tmp);
639 }
640 else
641 Forall_operands(it, expr)
642 replace_string_macros(*it, lhs, source_location);
643}
644
646 const exprt &pointer,
647 whatt what,
648 bool write,
649 const source_locationt &source_location)
650{
651 // take care of pointer typecasts now
652 if(pointer.id()==ID_typecast)
653 {
654 // cast from another pointer type?
655 if(to_typecast_expr(pointer).op().type().id() != ID_pointer)
656 return build_unknown(what, write);
657
658 // recursive call
659 return build(to_typecast_expr(pointer).op(), what, write, source_location);
660 }
661
663 if(build_wrap(pointer, str_struct, write))
665
666 exprt result=member(str_struct, what);
667
668 if(what==whatt::LENGTH || what==whatt::SIZE)
669 {
670 // adjust for offset
671 exprt offset = pointer_offset(pointer);
672 typet result_type = result.type();
675 typecast_exprt::conditional_cast(result, offset.type()), offset),
676 result_type);
677 }
678
679 return result;
680}
681
683{
684 abstraction_types_mapt::const_iterator map_entry =
685 abstraction_types_map.find(type);
687 return map_entry->second;
688
692
694 abstraction_types_map.insert(tmp.begin(), tmp.end());
695 map_entry = abstraction_types_map.find(type);
697 return map_entry->second;
698}
699
702{
703 abstraction_types_mapt::const_iterator known_entry = known.find(type);
704 if(known_entry!=known.end())
705 return known_entry->second;
706
707 ::std::pair<abstraction_types_mapt::iterator, bool> map_entry(
708 abstraction_types_map.insert(::std::make_pair(type, typet{ID_nil})));
709 if(!map_entry.second)
710 return map_entry.first->second;
711
712 if(type.id() == ID_array || type.id() == ID_pointer)
713 {
714 // char* or void* or char[]
715 if(is_char_type(type.subtype()) || type.subtype().id() == ID_empty)
716 map_entry.first->second=pointer_type(string_struct);
717 else
718 {
719 const typet &subt = build_abstraction_type_rec(type.subtype(), known);
720 if(!subt.is_nil())
721 {
722 if(type.id() == ID_array)
723 map_entry.first->second =
724 array_typet(subt, to_array_type(type).size());
725 else
726 map_entry.first->second=pointer_type(subt);
727 }
728 }
729 }
730 else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
731 {
734
736 for(const auto &comp : struct_union_type.components())
737 {
738 if(comp.get_anonymous())
739 continue;
741 if(subt.is_nil())
742 // also precludes structs with pointers to the same datatype
743 continue;
744
746 new_comp.back().set_name(comp.get_name());
747 new_comp.back().set_pretty_name(comp.get_pretty_name());
748 new_comp.back().type()=subt;
749 }
750 if(!new_comp.empty())
751 {
753 abstracted_type.components().swap(new_comp);
754
759 "",
761 existing_tag_symbol.location,
763 ns,
765 abstracted_type_symbol.is_type = true;
766 abstracted_type_symbol.is_lvalue = false;
767 abstracted_type_symbol.is_state_var = false;
768 abstracted_type_symbol.is_thread_local = true;
769 abstracted_type_symbol.is_file_local = true;
770 abstracted_type_symbol.is_auxiliary = false;
771 abstracted_type_symbol.is_macro = true;
772
773 if(type.id() == ID_struct_tag)
775 else
777 }
778 }
779
780 return map_entry.first->second;
781}
782
783bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
784{
785 const typet &abstract_type=build_abstraction_type(object.type());
786 if(abstract_type.is_nil())
787 return true;
788
789 if(object.id()==ID_typecast)
790 {
791 if(build(to_typecast_expr(object).op(), dest, write))
792 return true;
793
794 return dest.type() != abstract_type ||
795 (dest.type().id() == ID_array && abstract_type.id() == ID_pointer &&
796 dest.type().subtype() == abstract_type.subtype());
797 }
798
799 if(object.id()==ID_string_constant)
800 {
801 const std::string &str_value =
802 id2string(to_string_constant(object).get_value());
803 // make sure we handle the case of a string constant with string-terminating
804 // \0 in it
805 const std::size_t str_len =
806 std::min(str_value.size(), str_value.find('\0'));
808 }
809
810 if(object.id()==ID_array && is_char_type(object.type().subtype()))
811 return build_array(to_array_expr(object), dest, write);
812
813 // other constants aren't useful
814 if(object.is_constant())
815 return true;
816
817 if(object.id()==ID_symbol)
818 return build_symbol(to_symbol_expr(object), dest);
819
820 if(object.id()==ID_if)
821 return build_if(to_if_expr(object), dest, write);
822
823 if(object.id()==ID_member)
824 {
825 const member_exprt &o_mem=to_member_expr(object);
826 dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type);
827 return build_wrap(
828 o_mem.struct_op(), to_member_expr(dest).compound(), write);
829 }
830
831 if(object.id()==ID_dereference)
832 {
835 return build_wrap(
836 o_deref.pointer(), to_dereference_expr(dest).pointer(), write);
837 }
838
839 if(object.id()==ID_index)
840 {
841 const index_exprt &o_index=to_index_expr(object);
843 return build_wrap(o_index.array(), to_index_expr(dest).array(), write);
844 }
845
846 // handle pointer stuff
847 if(object.type().id()==ID_pointer)
848 return build_pointer(object, dest, write);
849
850 return true;
851}
852
854 exprt &dest, bool write)
855{
856 if_exprt new_if(o_if.cond(), exprt(), exprt());
857
858 // recursive calls
859 bool op1_err=build_wrap(o_if.true_case(), new_if.true_case(), write);
860 bool op2_err=build_wrap(o_if.false_case(), new_if.false_case(), write);
861 if(op1_err && op2_err)
862 return true;
863 // at least one of them gave proper results
864 if(op1_err)
865 {
866 new_if.type()=new_if.false_case().type();
867 new_if.true_case()=build_unknown(new_if.type(), write);
868 }
869 else if(op2_err)
870 {
871 new_if.type()=new_if.true_case().type();
872 new_if.false_case()=build_unknown(new_if.type(), write);
873 }
874 else
875 new_if.type()=new_if.true_case().type();
876
877 dest.swap(new_if);
878 return false;
879}
880
882 exprt &dest, bool write)
883{
884 PRECONDITION(is_char_type(object.type().element_type()));
885
886 // writing is invalid
887 if(write)
888 return true;
889
890 const exprt &a_size=to_array_type(object.type()).size();
891 const auto size = numeric_cast<mp_integer>(a_size);
892 // don't do anything, if we cannot determine the size
893 if(!size.has_value())
894 return true;
895 INVARIANT(
896 *size == object.operands().size(),
897 "wrong number of array object arguments");
898
899 exprt::operandst::const_iterator it=object.operands().begin();
900 for(mp_integer i = 0; i < *size; ++i, ++it)
901 if(it->is_zero())
902 return build_symbol_constant(i, *size, dest);
903
904 return true;
905}
906
908 exprt &dest, bool write)
909{
910 PRECONDITION(object.type().id() == ID_pointer);
911
912 pointer_arithmetict ptr(object);
913 if(ptr.pointer.id()==ID_address_of)
914 {
916
917 if(a.object().id()==ID_index)
918 return build_wrap(to_index_expr(a.object()).array(), dest, write);
919
920 // writing is invalid
921 if(write)
922 return true;
923
924 if(build_wrap(a.object(), dest, write))
925 return true;
927 return false;
928 }
929 else if(ptr.pointer.id()==ID_symbol &&
930 is_char_type(object.type().subtype()))
931 // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
932 // checks
933 return build_wrap(ptr.pointer, dest, write);
934
935 // we don't handle other pointer arithmetic
936 return true;
937}
938
940{
941 typet type=build_type(what);
942
943 if(write)
944 return exprt(ID_null_object, type);
945
946 exprt result;
947
948 switch(what)
949 {
950 case whatt::IS_ZERO:
951 result = from_integer(0, type);
952 break;
953
954 case whatt::LENGTH:
955 case whatt::SIZE:
957 break;
958 }
959
960 return result;
961}
962
964{
965 if(write)
966 return exprt(ID_null_object, type);
967
968 // create an uninitialized dummy symbol
969 // because of a lack of contextual information we can't build a nice name
970 // here, but moving that into locals should suffice for proper operation
971 irep_idt identifier=
972 "$tmp::nondet_str#str$"+std::to_string(++temporary_counter);
973 // ensure decl and initialization
974 locals[identifier]=identifier;
975
976 auxiliary_symbolt new_symbol;
977 new_symbol.type=type;
978 new_symbol.value.make_nil();
979 new_symbol.name=identifier;
980 new_symbol.module="$tmp";
981 new_symbol.base_name=identifier;
982 new_symbol.mode=ID_C;
983 new_symbol.pretty_name=identifier;
984
985 symbol_table.insert(std::move(new_symbol));
986
987 return ns.lookup(identifier).symbol_expr();
988}
989
991{
992 const symbolt &symbol=ns.lookup(sym.get_identifier());
993
995 CHECK_RETURN(!abstract_type.is_nil());
996
997 irep_idt identifier;
998
999 if(symbol.is_parameter)
1000 {
1001 const auto parameter_map_entry = parameter_map.find(symbol.name);
1003 return true;
1004 identifier = parameter_map_entry->second;
1005 }
1006 else if(symbol.is_static_lifetime)
1007 {
1008 std::string sym_suffix_before = sym_suffix;
1009 sym_suffix = "#str";
1010 identifier = id2string(symbol.name) + sym_suffix;
1011 if(symbol_table.symbols.find(identifier) == symbol_table.symbols.end())
1012 build_new_symbol(symbol, identifier, abstract_type);
1014 }
1015 else
1016 {
1017 identifier=id2string(symbol.name)+sym_suffix;
1018 if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
1019 build_new_symbol(symbol, identifier, abstract_type);
1020 }
1021
1022 const symbolt &str_symbol=ns.lookup(identifier);
1023 dest=str_symbol.symbol_expr();
1026
1027 return false;
1028}
1029
1031 const irep_idt &identifier, const typet &type)
1032{
1033 if(!symbol.is_static_lifetime)
1034 locals[symbol.name]=identifier;
1035
1036 auxiliary_symbolt new_symbol;
1037 new_symbol.type=type;
1038 new_symbol.value.make_nil();
1039 new_symbol.location=symbol.location;
1040 new_symbol.name=identifier;
1041 new_symbol.module=symbol.module;
1042 new_symbol.base_name=id2string(symbol.base_name)+sym_suffix;
1043 new_symbol.mode=symbol.mode;
1044 new_symbol.pretty_name=
1045 id2string(symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+
1046 sym_suffix;
1047 new_symbol.is_static_lifetime=symbol.is_static_lifetime;
1048 new_symbol.is_thread_local=symbol.is_thread_local;
1049
1050 symbol_table.insert(std::move(new_symbol));
1051
1052 if(symbol.is_static_lifetime)
1053 {
1056 dummy_loc->source_location_nonconst() = symbol.location;
1057 make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
1059 }
1060}
1061
1063 const mp_integer &zero_length,
1064 const mp_integer &buf_size,
1065 exprt &dest)
1066{
1067 irep_idt base="$string_constant_str_"+integer2string(zero_length)
1069 irep_idt identifier="string_abstraction::"+id2string(base);
1070
1071 if(symbol_table.symbols.find(identifier)==
1072 symbol_table.symbols.end())
1073 {
1074 auxiliary_symbolt new_symbol;
1075 new_symbol.type=string_struct;
1076 new_symbol.value.make_nil();
1077 new_symbol.name=identifier;
1078 new_symbol.base_name=base;
1079 new_symbol.mode=ID_C;
1080 new_symbol.pretty_name=base;
1081 new_symbol.is_static_lifetime=true;
1082 new_symbol.is_thread_local=false;
1083 new_symbol.is_file_local=false;
1084
1085 {
1086 struct_exprt value(
1091
1092 // initialization
1094 code_assignt(new_symbol.symbol_expr(), value)));
1095 }
1096
1097 symbol_table.insert(std::move(new_symbol));
1098 }
1099
1101
1102 return false;
1103}
1104
1106{
1107 while(lhs.id() == ID_typecast)
1108 {
1110 rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1111 lhs.swap(lhs_tc.op());
1112 }
1113
1114 if(lhs.id()==ID_minus)
1115 {
1116 // move op1 to rhs
1117 exprt rest = to_minus_expr(lhs).op0();
1118 rhs = plus_exprt(rhs, to_minus_expr(lhs).op1());
1119 rhs.type()=lhs.type();
1120 lhs=rest;
1121 }
1122
1123 while(lhs.id() == ID_typecast)
1124 {
1126 rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1127 lhs.swap(lhs_tc.op());
1128 }
1129}
1130
1133 const goto_programt::targett target)
1134{
1135 const exprt &lhs = target->assign_lhs();
1136 const exprt rhs = target->assign_rhs();
1137 const exprt *rhsp = &(target->assign_rhs());
1138
1139 while(rhsp->id()==ID_typecast)
1140 rhsp = &(to_typecast_expr(*rhsp).op());
1141
1143 if(abstract_type.is_nil())
1144 return target;
1145
1147 if(build_wrap(lhs, new_lhs, true))
1148 return target;
1149
1150 bool unknown=(abstract_type!=build_abstraction_type(rhsp->type()) ||
1151 build_wrap(rhs, new_rhs, false));
1152 if(unknown)
1154
1155 if(lhs.type().id()==ID_pointer && !unknown)
1156 {
1157 goto_programt::instructiont assignment;
1158 assignment = goto_programt::make_assignment(
1160 assignment.code_nonconst().add_source_location() =
1161 target->source_location();
1162 dest.insert_before_swap(target, assignment);
1163
1164 return std::next(target);
1165 }
1166 else
1167 {
1168 return value_assignments(dest, target, new_lhs, new_rhs);
1169 }
1170}
1171
1175{
1176 const exprt &lhs = target->assign_lhs();
1177 const exprt *rhsp = &(target->assign_rhs());
1178
1179 while(rhsp->id()==ID_typecast)
1180 rhsp = &(to_typecast_expr(*rhsp).op());
1181
1182 // we only care if the constant zero is assigned
1183 if(!rhsp->is_zero())
1184 return target;
1185
1186 // index into a character array
1187 if(lhs.id()==ID_index)
1188 {
1189 const index_exprt &i_lhs=to_index_expr(lhs);
1190
1191 exprt new_lhs;
1192 if(!build_wrap(i_lhs.array(), new_lhs, true))
1193 {
1195 INVARIANT(
1196 i2.is_not_nil(),
1197 "failed to create length-component for the left-hand-side");
1198
1199 exprt new_length=i_lhs.index();
1200 make_type(new_length, i2.type());
1201
1203 new_length, i2);
1204
1205 return char_assign(dest, target, new_lhs, i2, min_expr);
1206 }
1207 }
1208 else if(lhs.id()==ID_dereference)
1209 {
1210 pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
1211 exprt new_lhs;
1212 if(!build_wrap(ptr.pointer, new_lhs, true))
1213 {
1215 INVARIANT(
1216 i2.is_not_nil(),
1217 "failed to create length-component for the left-hand-side");
1218
1220 return
1222 dest,
1223 target,
1224 new_lhs,
1225 i2,
1226 ptr.offset.is_nil()?
1228 ptr.offset);
1229 }
1230 }
1231
1232 return target;
1233}
1234
1238 const exprt &new_lhs,
1239 const exprt &lhs,
1240 const exprt &rhs)
1241{
1243
1245 INVARIANT(
1246 i1.is_not_nil(),
1247 "failed to create is_zero-component for the left-hand-side");
1248
1250 code_assignt(i1, from_integer(1, i1.type())), target->source_location()));
1251 assignment1->code_nonconst().add_source_location() =
1252 target->source_location();
1253
1255 code_assignt(lhs, rhs), target->source_location()));
1256 assignment2->code_nonconst().add_source_location() =
1257 target->source_location();
1258
1260 assignment2->code_nonconst().op0(), assignment2->code_nonconst().op1());
1261
1262 dest.insert_before_swap(target, tmp);
1263 ++target;
1264 ++target;
1265
1266 return target;
1267}
1268
1272 const exprt &lhs,
1273 const exprt &rhs)
1274{
1275 if(rhs.id()==ID_if)
1276 return value_assignments_if(dest, target, lhs, to_if_expr(rhs));
1277
1278 PRECONDITION(lhs.type() == rhs.type());
1279
1280 if(lhs.type().id()==ID_array)
1281 {
1282 const exprt &a_size=to_array_type(lhs.type()).size();
1283 const auto size = numeric_cast<mp_integer>(a_size);
1284 // don't do anything, if we cannot determine the size
1285 if(!size.has_value())
1286 return target;
1287 for(mp_integer i = 0; i < *size; ++i)
1288 target=value_assignments(dest, target,
1289 index_exprt(lhs, from_integer(i, a_size.type())),
1290 index_exprt(rhs, from_integer(i, a_size.type())));
1291 }
1292 else if(lhs.type().id() == ID_pointer)
1293 return value_assignments(
1294 dest, target, dereference_exprt{lhs}, dereference_exprt{rhs});
1295 else if(lhs.type()==string_struct)
1296 return value_assignments_string_struct(dest, target, lhs, rhs);
1297 else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)
1298 {
1301
1302 for(const auto &comp : struct_union_type.components())
1303 {
1304 INVARIANT(
1305 !comp.get_name().empty(), "struct/union components must have a name");
1306
1307 target=value_assignments(dest, target,
1308 member_exprt(lhs, comp.get_name(), comp.type()),
1309 member_exprt(rhs, comp.get_name(), comp.type()));
1310 }
1311 }
1312
1313 return target;
1314}
1315
1319 const exprt &lhs, const if_exprt &rhs)
1320{
1322
1325 boolean_negate(rhs.cond()), target->source_location()));
1327 true_exprt(), target->source_location()));
1329 tmp.add(goto_programt::make_skip(target->source_location()));
1331 tmp.add(goto_programt::make_skip(target->source_location()));
1332
1333 goto_else->complete_goto(else_target);
1334 goto_out->complete_goto(out_target);
1335
1338
1340 ++last;
1341 dest.insert_before_swap(target, tmp);
1342 --last;
1343
1344 return last;
1345}
1346
1350 const exprt &lhs, const exprt &rhs)
1351{
1352 // copy all the values
1354
1355 {
1357 member(lhs, whatt::IS_ZERO),
1358 member(rhs, whatt::IS_ZERO),
1359 target->source_location()));
1360 assignment->code_nonconst().add_source_location() =
1361 target->source_location();
1362 }
1363
1364 {
1366 member(lhs, whatt::LENGTH),
1367 member(rhs, whatt::LENGTH),
1368 target->source_location()));
1369 assignment->code_nonconst().add_source_location() =
1370 target->source_location();
1371 }
1372
1373 {
1375 member(lhs, whatt::SIZE),
1376 member(rhs, whatt::SIZE),
1377 target->source_location()));
1378 assignment->code_nonconst().add_source_location() =
1379 target->source_location();
1380 }
1381
1383 ++last;
1384 dest.insert_before_swap(target, tmp);
1385 --last;
1386
1387 return last;
1388}
1389
1391{
1392 if(a.is_nil())
1393 return a;
1394
1396 a.type() == string_struct || is_ptr_string_struct(a.type()),
1397 "either the expression is not a string or it is not a pointer to one");
1398
1399 exprt struct_op=
1400 a.type().id()==ID_pointer?
1402
1403 irep_idt component_name;
1404
1405 switch(what)
1406 {
1407 case whatt::IS_ZERO: component_name="is_zero"; break;
1408 case whatt::SIZE: component_name="size"; break;
1409 case whatt::LENGTH: component_name="length"; break;
1410 }
1411
1412 return member_exprt(struct_op, component_name, build_type(what));
1413}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
unsignedbv_typet size_type()
Definition c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
typet c_bool_type()
Definition c_types.cpp:118
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Array constructor from list of elements.
Definition std_expr.h:1476
Array constructor from single element.
Definition std_expr.h:1411
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:790
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:147
exprt & op0()
Definition expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
A codet representing an assignment in the program.
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
const parameterst & parameters() const
Definition std_types.h:655
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
A collection of goto functions.
std::vector< irep_idt > parameter_identifierst
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
codet & code_nonconst()
Set the code represented by this instruction.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Definition std_expr.h:2226
exprt & cond()
Definition std_expr.h:2243
exprt & false_case()
Definition std_expr.h:2263
exprt & true_case()
Definition std_expr.h:2253
Array index operator.
Definition std_expr.h:1328
exprt & array()
Definition std_expr.h:1353
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Extract member of struct or union.
Definition std_expr.h:2667
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
Binary minus.
Definition std_expr.h:973
exprt & op2()
Definition std_expr.h:856
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:2874
The plus expression Associativity is not specified.
Definition std_expr.h:914
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Replace all uses of char * by a struct that carries that string, and also the underlying allocation a...
goto_programt::targett abstract(goto_programt &dest, goto_programt::targett it)
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
void declare_define_locals(goto_programt &dest)
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
static typet build_type(whatt what)
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
exprt build_unknown(whatt what, bool write)
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
bool is_ptr_string_struct(const typet &type) const
message_handlert & message_handler
::std::map< typet, typet > abstraction_types_mapt
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
symbol_exprt add_dummy_symbol_and_value(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const irep_idt &component_name, const typet &type, const typet &source_type)
bool build_wrap(const exprt &object, exprt &dest, bool write)
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
bool build_array(const array_exprt &object, exprt &dest, bool write)
void apply(goto_modelt &goto_model)
Apply string abstraction to goto_model.
bool build_symbol(const symbol_exprt &sym, exprt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
void operator()(goto_programt &dest)
abstraction_types_mapt abstraction_types_map
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
code_typet::parametert add_parameter(const symbolt &fct_symbol, const typet &type, const irep_idt &identifier)
bool build_pointer(const exprt &object, exprt &dest, bool write)
void abstract_function_call(goto_programt::targett it)
exprt member(const exprt &a, whatt what)
static bool has_string_macros(const exprt &expr)
void make_type(exprt &dest, const typet &type)
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
void add_str_parameters(symbolt &fct_symbol, goto_functiont::parameter_identifierst &parameter_identifiers)
bool is_char_type(const typet &type) const
symbol_tablet & symbol_table
const typet & build_abstraction_type(const typet &type)
Struct constructor from list of elements.
Definition std_expr.h:1722
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
Base type for structs and unions.
Definition std_types.h:62
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
Expression to hold a symbol (variable)
Definition std_expr.h:80
std::vector< irep_idt > sorted_symbol_names() const
Build and return a lexicographically sorted vector of symbol names from all symbols stored in this sy...
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
bool is_file_local
Definition symbol.h:66
bool is_static_lifetime
Definition symbol.h:65
bool is_parameter
Definition symbol.h:67
bool is_thread_local
Definition symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:2856
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
const exprt & op() const
Definition std_expr.h:293
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:177
int main()
Definition example.cpp:18
#define forall_operands(it, expr)
Definition expr.h:18
#define Forall_operands(it, expr)
Definition expr.h:25
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
dstringt irep_idt
Definition irep.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
exprt pointer_offset(const exprt &pointer)
Various predicates over pointers in programs.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1745
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1506
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:998
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
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 tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition std_types.h:434
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
static bool is_ptr_argument(const typet &type)
String Abstraction.
const string_constantt & to_string_constant(const exprt &expr)