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 &&
50 to_pointer_type(a_t).base_type()))
51 {
53 log.warning() << "warning: inconsistent abstract type for "
54 << object.pretty() << messaget::eom;
55 return true;
56 }
57
58 return false;
59}
60
62{
63 return type.id() == ID_pointer &&
65}
66
67static inline bool is_ptr_argument(const typet &type)
68{
69 return type.id()==ID_pointer;
70}
71
73 goto_modelt &goto_model,
74 message_handlert &message_handler)
75{
76 string_abstractiont{goto_model, message_handler}.apply();
77}
78
80 goto_modelt &goto_model,
81 message_handlert &_message_handler)
82 : sym_suffix("#str$fcn"),
83 goto_model(goto_model),
84 ns(goto_model.symbol_table),
85 temporary_counter(0),
86 message_handler(_message_handler)
87{
88 struct_typet s({{"is_zero", build_type(whatt::IS_ZERO)},
89 {"length", build_type(whatt::LENGTH)},
90 {"size", build_type(whatt::SIZE)}});
91 s.components()[0].set_pretty_name("is_zero");
92 s.components()[1].set_pretty_name("length");
93 s.components()[2].set_pretty_name("size");
94
95 symbolt &struct_symbol = get_fresh_aux_symbol(
96 s,
97 "tag-",
98 "string_struct",
100 ID_C,
101 ns,
103 struct_symbol.is_type = true;
104 struct_symbol.is_lvalue = false;
105 struct_symbol.is_state_var = false;
106 struct_symbol.is_thread_local = true;
107 struct_symbol.is_file_local = true;
108 struct_symbol.is_auxiliary = false;
109 struct_symbol.is_macro = true;
110
111 string_struct = struct_tag_typet{struct_symbol.name};
112}
113
115{
116 typet type;
117
118 // clang-format off
119 switch(what)
120 {
121 case whatt::IS_ZERO: type=c_bool_type(); break;
122 case whatt::LENGTH: type=size_type(); break;
123 case whatt::SIZE: type=size_type(); break;
124 }
125 // clang-format on
126
127 return type;
128}
129
131{
133 symbol_tablet &symbol_table = goto_model.symbol_table;
134
135 // iterate over all previously known symbols as the body of the loop modifies
136 // the symbol table and can thus invalidate iterators
137 for(auto &sym_name : symbol_table.sorted_symbol_names())
138 {
139 symbolt &symbol = symbol_table.get_writeable_ref(sym_name);
140 const typet &type = symbol.type;
141
142 if(type.id() != ID_code)
143 continue;
144
145 sym_suffix = "#str$" + id2string(sym_name);
146
147 goto_functionst::function_mapt::iterator fct_entry =
148 dest.function_map.find(sym_name);
149 if(fct_entry != dest.function_map.end())
150 {
151 add_str_parameters(symbol, fct_entry->second.parameter_identifiers);
152 }
153 else
154 {
156 to_code_type(type).parameters().size(), irep_idt{});
157 add_str_parameters(symbol, dummy);
158 }
159 }
160
161 for(auto &gf_entry : dest.function_map)
162 {
163 sym_suffix = "#str$" + id2string(gf_entry.first);
164 abstract(gf_entry.second.body);
165 }
166
167 // do we have a main?
168 goto_functionst::function_mapt::iterator
169 m_it=dest.function_map.find(dest.entry_point());
170
171 if(m_it!=dest.function_map.end())
172 {
173 goto_programt &main=m_it->second.body;
174
175 // do initialization
177 main.swap(initialization);
179 }
180}
181
183{
184 abstract(dest);
185
186 // do initialization
188 dest.swap(initialization);
190}
191
193 symbolt &fct_symbol,
194 goto_functiont::parameter_identifierst &parameter_identifiers)
195{
196 code_typet &fct_type = to_code_type(fct_symbol.type);
197 PRECONDITION(fct_type.parameters().size() == parameter_identifiers.size());
198
200
201 goto_functiont::parameter_identifierst::const_iterator param_id_it =
202 parameter_identifiers.begin();
203 for(const auto &parameter : fct_type.parameters())
204 {
205 const typet &abstract_type = build_abstraction_type(parameter.type());
206 if(abstract_type.is_nil())
207 continue;
208
209 str_args.push_back(add_parameter(fct_symbol, abstract_type, *param_id_it));
210 ++param_id_it;
211 }
212
213 for(const auto &new_param : str_args)
214 parameter_identifiers.push_back(new_param.get_identifier());
215 fct_type.parameters().insert(
216 fct_type.parameters().end(), str_args.begin(), str_args.end());
217}
218
220 const symbolt &fct_symbol,
221 const typet &type,
222 const irep_idt &identifier)
223{
224 typet final_type=is_ptr_argument(type)?
225 type:pointer_type(type);
226
227 symbolt &param_symbol = get_fresh_aux_symbol(
228 final_type,
229 id2string(identifier.empty() ? fct_symbol.name : identifier),
230 id2string(
231 identifier.empty() ? fct_symbol.base_name
232 : ns.lookup(identifier).base_name) +
233 "#str",
234 fct_symbol.location,
235 fct_symbol.mode,
237 param_symbol.is_parameter = true;
238 param_symbol.value.make_nil();
239
240 code_typet::parametert str_parameter{final_type};
241 str_parameter.add_source_location() = fct_symbol.location;
242 str_parameter.set_base_name(param_symbol.base_name);
243 str_parameter.set_identifier(param_symbol.name);
244
245 if(!identifier.empty())
246 parameter_map.insert(std::make_pair(identifier, param_symbol.name));
247
248 return str_parameter;
249}
250
252{
253 locals.clear();
254
256 it=abstract(dest, it);
257
258 if(locals.empty())
259 return;
260
261 // go over it again for the newly added locals
263 locals.clear();
264}
265
267{
268 typedef std::unordered_map<irep_idt, goto_programt::targett> available_declst;
269 available_declst available_decls;
270
272 if(it->is_decl())
273 // same name may exist several times due to inlining, make sure the first
274 // declaration is used
275 available_decls.insert(
276 std::make_pair(it->decl_symbol().get_identifier(), it));
277
278 // declare (and, if necessary, define) locals
279 for(const auto &l : locals)
280 {
281 goto_programt::targett ref_instr=dest.instructions.begin();
282 bool has_decl=false;
283
284 available_declst::const_iterator entry=available_decls.find(l.first);
285
286 if(available_declst::const_iterator(available_decls.end())!=entry)
287 {
288 ref_instr=entry->second;
289 has_decl=true;
290 }
291
292 goto_programt tmp;
293 make_decl_and_def(tmp, ref_instr, l.second, l.first);
294
295 if(has_decl)
296 ++ref_instr;
297 dest.insert_before_swap(ref_instr, tmp);
298 }
299}
300
302 goto_programt::targett ref_instr,
303 const irep_idt &identifier,
304 const irep_idt &source_sym)
305{
306 const symbolt &symbol=ns.lookup(identifier);
307 symbol_exprt sym_expr=symbol.symbol_expr();
308 code_declt decl{sym_expr};
309 decl.add_source_location() = ref_instr->source_location();
310 dest.add(
311 goto_programt::make_decl(std::move(decl), ref_instr->source_location()));
312
313 exprt val=symbol.value;
314 // initialize pointers with suitable objects
315 if(val.is_nil())
316 {
317 const symbolt &orig=ns.lookup(source_sym);
318 val = make_val_or_dummy_rec(dest, ref_instr, symbol, orig.type);
319 }
320
321 // may still be nil (structs, then assignments have been done already)
322 if(val.is_not_nil())
323 {
324 code_assignt assignment{sym_expr, val, ref_instr->source_location()};
325 dest.add(
326 goto_programt::make_assignment(assignment, ref_instr->source_location()));
327 }
328}
329
331 goto_programt::targett ref_instr,
332 const symbolt &symbol, const typet &source_type)
333{
334 if(symbol.type.id() == ID_array || symbol.type.id() == ID_pointer)
335 {
336 const typet &source_subt = is_ptr_string_struct(symbol.type)
337 ? source_type
338 : to_type_with_subtype(source_type).subtype();
340 dest,
341 ref_instr,
342 symbol,
343 irep_idt(),
345 source_subt);
346
347 if(symbol.type.id() == ID_array)
348 return array_of_exprt(sym_expr, to_array_type(symbol.type));
349 else
350 return address_of_exprt(sym_expr);
351 }
352 else if(
353 symbol.type.id() == ID_union_tag ||
354 (symbol.type.id() == ID_struct_tag && symbol.type != string_struct))
355 {
356 const struct_union_typet &su_source =
357 to_struct_union_type(ns.follow(source_type));
358 const struct_union_typet::componentst &s_components=
359 su_source.components();
360 const struct_union_typet &struct_union_type =
362 const struct_union_typet::componentst &components=
363 struct_union_type.components();
364 unsigned seen=0;
365
366 struct_union_typet::componentst::const_iterator it2=components.begin();
367 for(struct_union_typet::componentst::const_iterator
368 it=s_components.begin();
369 it!=s_components.end() && it2!=components.end();
370 ++it)
371 {
372 if(it->get_name()!=it2->get_name())
373 continue;
374
375 if(
376 it2->type().id() == ID_pointer || it2->type().id() == ID_array ||
377 it2->type().id() == ID_struct_tag || it2->type().id() == ID_union_tag)
378 {
380 dest, ref_instr, symbol, it2->get_name(), it2->type(), it->type());
381
382 member_exprt member(symbol.symbol_expr(), it2->get_name(), it2->type());
383
384 code_assignt assignment{member, sym_expr, ref_instr->source_location()};
386 code_assignt(member, sym_expr), ref_instr->source_location()));
387 }
388
389 ++seen;
390 ++it2;
391 }
392
393 INVARIANT(
394 components.size() == seen,
395 "some of the symbol's component names were not found in the source");
396 }
397
398 return nil_exprt();
399}
400
402 goto_programt &dest,
403 goto_programt::targett ref_instr,
404 const symbolt &symbol,
405 const irep_idt &component_name,
406 const typet &type,
407 const typet &source_type)
408{
409 std::string suffix="$strdummy";
410 if(!component_name.empty())
411 suffix="#"+id2string(component_name)+suffix;
412
413 irep_idt dummy_identifier=id2string(symbol.name)+suffix;
414
415 auxiliary_symbolt new_symbol;
416 new_symbol.type=type;
417 new_symbol.value.make_nil();
418 new_symbol.location = ref_instr->source_location();
419 new_symbol.name=dummy_identifier;
420 new_symbol.module=symbol.module;
421 new_symbol.base_name=id2string(symbol.base_name)+suffix;
422 new_symbol.mode=symbol.mode;
423 new_symbol.pretty_name=id2string(
424 symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+suffix;
425
426 symbol_exprt sym_expr=new_symbol.symbol_expr();
427
428 // make sure it is declared before the recursive call
429 code_declt decl{sym_expr};
430 decl.add_source_location() = ref_instr->source_location();
431 dest.add(
432 goto_programt::make_decl(std::move(decl), ref_instr->source_location()));
433
434 // set the value - may be nil
435 if(
436 source_type.id() == ID_array &&
437 is_char_type(to_array_type(source_type).element_type()) &&
438 type == string_struct)
439 {
440 new_symbol.value = struct_exprt(
443 to_array_type(source_type).size().id() == ID_infinity
444 ? build_unknown(whatt::SIZE, false)
445 : to_array_type(source_type).size()},
447
449 }
450 else
451 new_symbol.value=
452 make_val_or_dummy_rec(dest, ref_instr, new_symbol, source_type);
453
454 if(new_symbol.value.is_not_nil())
455 {
456 code_assignt assignment{
457 sym_expr, new_symbol.value, ref_instr->source_location()};
458 dest.add(
459 goto_programt::make_assignment(assignment, ref_instr->source_location()));
460 }
461
462 goto_model.symbol_table.insert(std::move(new_symbol));
463
464 return sym_expr;
465}
466
468 goto_programt &dest,
470{
471 switch(it->type())
472 {
473 case ASSIGN:
474 it=abstract_assign(dest, it);
475 break;
476
477 case GOTO:
478 case ASSERT:
479 case ASSUME:
480 if(has_string_macros(it->condition()))
482 it->condition_nonconst(), false, it->source_location());
483 break;
484
485 case FUNCTION_CALL:
487 break;
488
489 case SET_RETURN_VALUE:
490 // use remove_returns
492 break;
493
494 case END_FUNCTION:
495 case START_THREAD:
496 case END_THREAD:
497 case ATOMIC_BEGIN:
498 case ATOMIC_END:
499 case DECL:
500 case DEAD:
501 case CATCH:
502 case THROW:
503 case SKIP:
504 case OTHER:
505 case LOCATION:
506 break;
507
508 case INCOMPLETE_GOTO:
511 break;
512 }
513
514 return it;
515}
516
518 goto_programt &dest,
520{
521 {
522 exprt &lhs = target->assign_lhs_nonconst();
523 exprt &rhs = target->assign_rhs_nonconst();
524
525 if(has_string_macros(lhs))
526 {
527 replace_string_macros(lhs, true, target->source_location());
528 move_lhs_arithmetic(lhs, rhs);
529 }
530
531 if(has_string_macros(rhs))
532 replace_string_macros(rhs, false, target->source_location());
533 }
534
535 const typet &type = target->assign_lhs().type();
536
537 if(type.id() == ID_pointer || type.id() == ID_array)
538 return abstract_pointer_assign(dest, target);
539 else if(is_char_type(type))
540 return abstract_char_assign(dest, target);
541
542 return target;
543}
544
547{
548 auto arguments = as_const(*target).call_arguments();
550
551 for(const auto &arg : arguments)
552 {
553 const typet &abstract_type = build_abstraction_type(arg.type());
554 if(abstract_type.is_nil())
555 continue;
556
557 str_args.push_back(exprt());
558 // if function takes void*, build for `arg` will fail if actual parameter
559 // is of some other pointer type; then just introduce an unknown
560 if(build_wrap(arg, str_args.back(), false))
561 str_args.back()=build_unknown(abstract_type, false);
562 // array -> pointer translation
563 if(str_args.back().type().id()==ID_array &&
564 abstract_type.id()==ID_pointer)
565 {
566 INVARIANT(
567 to_array_type(str_args.back().type()).element_type() ==
568 to_pointer_type(abstract_type).base_type(),
569 "argument array type differs from formal parameter pointer type");
570
571 index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
572 str_args.back()=address_of_exprt(idx);
573 }
574
575 if(!is_ptr_argument(abstract_type))
576 str_args.back()=address_of_exprt(str_args.back());
577 }
578
579 if(!str_args.empty())
580 {
581 arguments.insert(arguments.end(), str_args.begin(), str_args.end());
582
583 auto &parameters =
584 to_code_type(target->call_function().type()).parameters();
585 for(const auto &arg : str_args)
586 parameters.push_back(code_typet::parametert{arg.type()});
587
588 target->call_arguments() = std::move(arguments);
589 }
590}
591
593{
594 if(expr.id()=="is_zero_string" ||
595 expr.id()=="zero_string_length" ||
596 expr.id()=="buffer_size")
597 return true;
598
599 for(const auto &op : expr.operands())
600 {
601 if(has_string_macros(op))
602 return true;
603 }
604
605 return false;
606}
607
609 exprt &expr,
610 bool lhs,
611 const source_locationt &source_location)
612{
613 if(expr.id()=="is_zero_string")
614 {
615 PRECONDITION(expr.operands().size() == 1);
616 exprt tmp =
617 build(to_unary_expr(expr).op(), whatt::IS_ZERO, lhs, source_location);
618 expr.swap(tmp);
619 }
620 else if(expr.id()=="zero_string_length")
621 {
622 PRECONDITION(expr.operands().size() == 1);
623 exprt tmp =
624 build(to_unary_expr(expr).op(), whatt::LENGTH, lhs, source_location);
625 expr.swap(tmp);
626 }
627 else if(expr.id()=="buffer_size")
628 {
629 PRECONDITION(expr.operands().size() == 1);
630 exprt tmp =
631 build(to_unary_expr(expr).op(), whatt::SIZE, false, source_location);
632 expr.swap(tmp);
633 }
634 else
635 Forall_operands(it, expr)
636 replace_string_macros(*it, lhs, source_location);
637}
638
640 const exprt &pointer,
641 whatt what,
642 bool write,
643 const source_locationt &source_location)
644{
645 // take care of pointer typecasts now
646 if(pointer.id()==ID_typecast)
647 {
648 const exprt &op = to_typecast_expr(pointer).op();
649
650 // cast from another pointer type?
651 if(
652 op.type().id() != ID_pointer ||
654 {
655 return build_unknown(what, write);
656 }
657
658 // recursive call
659 return build(op, what, write, source_location);
660 }
661
662 exprt str_struct;
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);
686 if(map_entry!=abstraction_types_map.end())
687 return map_entry->second;
688
690 tmp.swap(abstraction_types_map);
692
693 abstraction_types_map.swap(tmp);
694 abstraction_types_map.insert(tmp.begin(), tmp.end());
695 map_entry = abstraction_types_map.find(type);
696 CHECK_RETURN(map_entry != abstraction_types_map.end());
697 return map_entry->second;
698}
699
701 const abstraction_types_mapt &known)
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(
716 is_char_type(to_type_with_subtype(type).subtype()) ||
717 to_type_with_subtype(type).subtype().id() == ID_empty)
718 map_entry.first->second=pointer_type(string_struct);
719 else
720 {
721 const typet &subt =
722 build_abstraction_type_rec(to_type_with_subtype(type).subtype(), known);
723 if(!subt.is_nil())
724 {
725 if(type.id() == ID_array)
726 map_entry.first->second =
727 array_typet(subt, to_array_type(type).size());
728 else
729 map_entry.first->second=pointer_type(subt);
730 }
731 }
732 }
733 else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
734 {
735 const struct_union_typet &struct_union_type =
737
739 for(const auto &comp : struct_union_type.components())
740 {
741 if(comp.get_anonymous())
742 continue;
743 typet subt=build_abstraction_type_rec(comp.type(), known);
744 if(subt.is_nil())
745 // also precludes structs with pointers to the same datatype
746 continue;
747
748 new_comp.push_back(struct_union_typet::componentt());
749 new_comp.back().set_name(comp.get_name());
750 new_comp.back().set_pretty_name(comp.get_pretty_name());
751 new_comp.back().type()=subt;
752 }
753 if(!new_comp.empty())
754 {
755 struct_union_typet abstracted_type = struct_union_type;
756 abstracted_type.components().swap(new_comp);
757
758 const symbolt &existing_tag_symbol =
759 ns.lookup(to_tag_type(type).get_identifier());
760 symbolt &abstracted_type_symbol = get_fresh_aux_symbol(
761 abstracted_type,
762 "",
763 id2string(existing_tag_symbol.name),
764 existing_tag_symbol.location,
765 existing_tag_symbol.mode,
766 ns,
768 abstracted_type_symbol.is_type = true;
769 abstracted_type_symbol.is_lvalue = false;
770 abstracted_type_symbol.is_state_var = false;
771 abstracted_type_symbol.is_thread_local = true;
772 abstracted_type_symbol.is_file_local = true;
773 abstracted_type_symbol.is_auxiliary = false;
774 abstracted_type_symbol.is_macro = true;
775
776 if(type.id() == ID_struct_tag)
777 map_entry.first->second = struct_tag_typet{abstracted_type_symbol.name};
778 else
779 map_entry.first->second = union_tag_typet{abstracted_type_symbol.name};
780 }
781 }
782
783 return map_entry.first->second;
784}
785
786bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
787{
788 const typet &abstract_type=build_abstraction_type(object.type());
789 if(abstract_type.is_nil())
790 return true;
791
792 if(object.id()==ID_typecast)
793 {
794 if(build(to_typecast_expr(object).op(), dest, write))
795 return true;
796
797 return dest.type() != abstract_type ||
798 (dest.type().id() == ID_array && abstract_type.id() == ID_pointer &&
799 to_array_type(dest.type()).element_type() ==
800 to_pointer_type(abstract_type).base_type());
801 }
802
803 if(object.id()==ID_string_constant)
804 {
805 const std::string &str_value =
806 id2string(to_string_constant(object).get_value());
807 // make sure we handle the case of a string constant with string-terminating
808 // \0 in it
809 const std::size_t str_len =
810 std::min(str_value.size(), str_value.find('\0'));
811 return build_symbol_constant(str_len, str_len+1, dest);
812 }
813
814 if(
815 object.id() == ID_array &&
816 is_char_type(to_array_type(object.type()).element_type()))
817 return build_array(to_array_expr(object), dest, write);
818
819 // other constants aren't useful
820 if(object.is_constant())
821 return true;
822
823 if(object.id()==ID_symbol)
824 return build_symbol(to_symbol_expr(object), dest);
825
826 if(object.id()==ID_if)
827 return build_if(to_if_expr(object), dest, write);
828
829 if(object.id()==ID_member)
830 {
831 const member_exprt &o_mem=to_member_expr(object);
832 exprt compound;
833 if(build_wrap(o_mem.struct_op(), compound, write))
834 return true;
835 dest = member_exprt{
836 std::move(compound), o_mem.get_component_name(), abstract_type};
837 return false;
838 }
839
840 if(object.id()==ID_dereference)
841 {
842 const dereference_exprt &o_deref=to_dereference_expr(object);
843 exprt pointer;
844 if(build_wrap(o_deref.pointer(), pointer, write))
845 return true;
846 dest = dereference_exprt{std::move(pointer)};
847 return false;
848 }
849
850 if(object.id()==ID_index)
851 {
852 const index_exprt &o_index=to_index_expr(object);
853 exprt array;
854 if(build_wrap(o_index.array(), array, write))
855 return true;
856 dest = index_exprt{std::move(array), o_index.index()};
857 return false;
858 }
859
860 // handle pointer stuff
861 if(object.type().id()==ID_pointer)
862 return build_pointer(object, dest, write);
863
864 return true;
865}
866
868 exprt &dest, bool write)
869{
870 if_exprt new_if(o_if.cond(), exprt(), exprt());
871
872 // recursive calls
873 bool op1_err=build_wrap(o_if.true_case(), new_if.true_case(), write);
874 bool op2_err=build_wrap(o_if.false_case(), new_if.false_case(), write);
875 if(op1_err && op2_err)
876 return true;
877 // at least one of them gave proper results
878 if(op1_err)
879 {
880 new_if.type()=new_if.false_case().type();
881 new_if.true_case()=build_unknown(new_if.type(), write);
882 }
883 else if(op2_err)
884 {
885 new_if.type()=new_if.true_case().type();
886 new_if.false_case()=build_unknown(new_if.type(), write);
887 }
888 else
889 new_if.type()=new_if.true_case().type();
890
891 dest.swap(new_if);
892 return false;
893}
894
896 exprt &dest, bool write)
897{
898 PRECONDITION(is_char_type(object.type().element_type()));
899
900 // writing is invalid
901 if(write)
902 return true;
903
904 const exprt &a_size=to_array_type(object.type()).size();
905 const auto size = numeric_cast<mp_integer>(a_size);
906 // don't do anything, if we cannot determine the size
907 if(!size.has_value())
908 return true;
909 INVARIANT(
910 *size == object.operands().size(),
911 "wrong number of array object arguments");
912
913 exprt::operandst::const_iterator it=object.operands().begin();
914 for(mp_integer i = 0; i < *size; ++i, ++it)
915 if(it->is_zero())
916 return build_symbol_constant(i, *size, dest);
917
918 return true;
919}
920
922 exprt &dest, bool write)
923{
924 PRECONDITION(object.type().id() == ID_pointer);
925
926 pointer_arithmetict ptr(object);
927 if(ptr.pointer.id()==ID_address_of)
928 {
930
931 if(a.object().id()==ID_index)
932 return build_wrap(to_index_expr(a.object()).array(), dest, write);
933
934 // writing is invalid
935 if(write)
936 return true;
937
938 if(build_wrap(a.object(), dest, write))
939 return true;
940 dest=address_of_exprt(dest);
941 return false;
942 }
943 else if(
944 ptr.pointer.id() == ID_symbol &&
945 is_char_type(to_pointer_type(object.type()).base_type()))
946 // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
947 // checks
948 return build_wrap(ptr.pointer, dest, write);
949
950 // we don't handle other pointer arithmetic
951 return true;
952}
953
955{
956 typet type=build_type(what);
957
958 if(write)
959 return exprt(ID_null_object, type);
960
961 exprt result;
962
963 switch(what)
964 {
965 case whatt::IS_ZERO:
966 result = from_integer(0, type);
967 break;
968
969 case whatt::LENGTH:
970 case whatt::SIZE:
972 break;
973 }
974
975 return result;
976}
977
979{
980 if(write)
981 return exprt(ID_null_object, type);
982
983 // create an uninitialized dummy symbol
984 // because of a lack of contextual information we can't build a nice name
985 // here, but moving that into locals should suffice for proper operation
986 irep_idt identifier=
987 "$tmp::nondet_str#str$"+std::to_string(++temporary_counter);
988 // ensure decl and initialization
989 locals[identifier]=identifier;
990
991 auxiliary_symbolt new_symbol;
992 new_symbol.type=type;
993 new_symbol.value.make_nil();
994 new_symbol.name=identifier;
995 new_symbol.module="$tmp";
996 new_symbol.base_name=identifier;
997 new_symbol.mode=ID_C;
998 new_symbol.pretty_name=identifier;
999
1000 goto_model.symbol_table.insert(std::move(new_symbol));
1001
1002 return ns.lookup(identifier).symbol_expr();
1003}
1004
1006{
1007 const symbolt &symbol=ns.lookup(sym.get_identifier());
1008
1009 const typet &abstract_type=build_abstraction_type(symbol.type);
1010 CHECK_RETURN(!abstract_type.is_nil());
1011
1012 irep_idt identifier;
1013
1014 if(symbol.is_parameter)
1015 {
1016 const auto parameter_map_entry = parameter_map.find(symbol.name);
1017 if(parameter_map_entry == parameter_map.end())
1018 return true;
1019 identifier = parameter_map_entry->second;
1020 }
1021 else if(symbol.is_static_lifetime)
1022 {
1023 std::string sym_suffix_before = sym_suffix;
1024 sym_suffix = "#str";
1025 identifier = id2string(symbol.name) + sym_suffix;
1026 if(!goto_model.symbol_table.has_symbol(identifier))
1027 build_new_symbol(symbol, identifier, abstract_type);
1028 sym_suffix = sym_suffix_before;
1029 }
1030 else
1031 {
1032 identifier=id2string(symbol.name)+sym_suffix;
1033 if(!goto_model.symbol_table.has_symbol(identifier))
1034 build_new_symbol(symbol, identifier, abstract_type);
1035 }
1036
1037 const symbolt &str_symbol=ns.lookup(identifier);
1038 dest=str_symbol.symbol_expr();
1039 if(symbol.is_parameter && !is_ptr_argument(abstract_type))
1040 dest = dereference_exprt{dest};
1041
1042 return false;
1043}
1044
1046 const irep_idt &identifier, const typet &type)
1047{
1048 if(!symbol.is_static_lifetime)
1049 locals[symbol.name]=identifier;
1050
1051 auxiliary_symbolt new_symbol;
1052 new_symbol.type=type;
1053 new_symbol.value.make_nil();
1054 new_symbol.location=symbol.location;
1055 new_symbol.name=identifier;
1056 new_symbol.module=symbol.module;
1057 new_symbol.base_name=id2string(symbol.base_name)+sym_suffix;
1058 new_symbol.mode=symbol.mode;
1059 new_symbol.pretty_name=
1060 id2string(symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+
1061 sym_suffix;
1062 new_symbol.is_static_lifetime=symbol.is_static_lifetime;
1063 new_symbol.is_thread_local=symbol.is_thread_local;
1064
1065 goto_model.symbol_table.insert(std::move(new_symbol));
1066
1067 if(symbol.is_static_lifetime)
1068 {
1069 goto_programt::targett dummy_loc =
1071 codet{ID_nil},
1072 symbol.location,
1074 {},
1075 {}});
1076 make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
1077 initialization.instructions.erase(dummy_loc);
1078 }
1079}
1080
1082 const mp_integer &zero_length,
1083 const mp_integer &buf_size,
1084 exprt &dest)
1085{
1086 irep_idt base="$string_constant_str_"+integer2string(zero_length)
1087 +"_"+integer2string(buf_size);
1088 irep_idt identifier="string_abstraction::"+id2string(base);
1089
1090 if(!goto_model.symbol_table.has_symbol(identifier))
1091 {
1092 auxiliary_symbolt new_symbol;
1093 new_symbol.type=string_struct;
1094 new_symbol.value.make_nil();
1095 new_symbol.name=identifier;
1096 new_symbol.base_name=base;
1097 new_symbol.mode=ID_C;
1098 new_symbol.pretty_name=base;
1099 new_symbol.is_static_lifetime=true;
1100 new_symbol.is_thread_local=false;
1101 new_symbol.is_file_local=false;
1102
1103 {
1104 struct_exprt value(
1106 from_integer(zero_length, build_type(whatt::LENGTH)),
1107 from_integer(buf_size, build_type(whatt::SIZE))},
1109
1110 // initialization
1112 code_assignt(new_symbol.symbol_expr(), value)));
1113 }
1114
1115 goto_model.symbol_table.insert(std::move(new_symbol));
1116 }
1117
1118 dest=address_of_exprt(symbol_exprt(identifier, string_struct));
1119
1120 return false;
1121}
1122
1124{
1125 while(lhs.id() == ID_typecast)
1126 {
1127 typecast_exprt lhs_tc = to_typecast_expr(lhs);
1128 rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1129 lhs.swap(lhs_tc.op());
1130 }
1131
1132 if(lhs.id()==ID_minus)
1133 {
1134 // move op1 to rhs
1135 exprt rest = to_minus_expr(lhs).op0();
1136 rhs = plus_exprt(rhs, to_minus_expr(lhs).op1());
1137 rhs.type()=lhs.type();
1138 lhs=rest;
1139 }
1140
1141 while(lhs.id() == ID_typecast)
1142 {
1143 typecast_exprt lhs_tc = to_typecast_expr(lhs);
1144 rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1145 lhs.swap(lhs_tc.op());
1146 }
1147}
1148
1150 goto_programt &dest,
1151 const goto_programt::targett target)
1152{
1153 const exprt &lhs = target->assign_lhs();
1154 const exprt rhs = target->assign_rhs();
1155 const exprt *rhsp = &(target->assign_rhs());
1156
1157 while(rhsp->id()==ID_typecast)
1158 rhsp = &(to_typecast_expr(*rhsp).op());
1159
1160 const typet &abstract_type=build_abstraction_type(lhs.type());
1161 if(abstract_type.is_nil())
1162 return target;
1163
1164 exprt new_lhs, new_rhs;
1165 if(build_wrap(lhs, new_lhs, true))
1166 return target;
1167
1168 bool unknown=(abstract_type!=build_abstraction_type(rhsp->type()) ||
1169 build_wrap(rhs, new_rhs, false));
1170 if(unknown)
1171 new_rhs=build_unknown(abstract_type, false);
1172
1173 if(lhs.type().id()==ID_pointer && !unknown)
1174 {
1176 code_assignt(new_lhs, new_rhs, target->source_location()),
1177 target->source_location());
1178 dest.insert_before_swap(target, assignment);
1179
1180 return std::next(target);
1181 }
1182 else
1183 {
1184 return value_assignments(dest, target, new_lhs, new_rhs);
1185 }
1186}
1187
1189 goto_programt &dest,
1191{
1192 const exprt &lhs = target->assign_lhs();
1193 const exprt *rhsp = &(target->assign_rhs());
1194
1195 while(rhsp->id()==ID_typecast)
1196 rhsp = &(to_typecast_expr(*rhsp).op());
1197
1198 // we only care if the constant zero is assigned
1199 if(!rhsp->is_zero())
1200 return target;
1201
1202 // index into a character array
1203 if(lhs.id()==ID_index)
1204 {
1205 const index_exprt &i_lhs=to_index_expr(lhs);
1206
1207 exprt new_lhs;
1208 if(!build_wrap(i_lhs.array(), new_lhs, true))
1209 {
1210 exprt i2=member(new_lhs, whatt::LENGTH);
1211 INVARIANT(
1212 i2.is_not_nil(),
1213 "failed to create length-component for the left-hand-side");
1214
1215 exprt new_length=i_lhs.index();
1216 make_type(new_length, i2.type());
1217
1218 if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
1219 new_length, i2);
1220
1221 return char_assign(dest, target, new_lhs, i2, min_expr);
1222 }
1223 }
1224 else if(lhs.id()==ID_dereference)
1225 {
1226 pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
1227 exprt new_lhs;
1228 if(!build_wrap(ptr.pointer, new_lhs, true))
1229 {
1230 const exprt i2=member(new_lhs, whatt::LENGTH);
1231 INVARIANT(
1232 i2.is_not_nil(),
1233 "failed to create length-component for the left-hand-side");
1234
1236 return
1238 dest,
1239 target,
1240 new_lhs,
1241 i2,
1242 ptr.offset.is_nil()?
1244 ptr.offset);
1245 }
1246 }
1247
1248 return target;
1249}
1250
1252 goto_programt &dest,
1254 const exprt &new_lhs,
1255 const exprt &lhs,
1256 const exprt &rhs)
1257{
1258 goto_programt tmp;
1259
1260 const exprt i1=member(new_lhs, whatt::IS_ZERO);
1261 INVARIANT(
1262 i1.is_not_nil(),
1263 "failed to create is_zero-component for the left-hand-side");
1264
1266 code_assignt(i1, from_integer(1, i1.type()), target->source_location()),
1267 target->source_location()));
1268
1269 code_assignt assignment{lhs, rhs, target->source_location()};
1270 move_lhs_arithmetic(assignment.lhs(), assignment.rhs());
1271 tmp.add(
1272 goto_programt::make_assignment(assignment, target->source_location()));
1273
1274 dest.insert_before_swap(target, tmp);
1275 ++target;
1276 ++target;
1277
1278 return target;
1279}
1280
1282 goto_programt &dest,
1284 const exprt &lhs,
1285 const exprt &rhs)
1286{
1287 if(rhs.id()==ID_if)
1288 return value_assignments_if(dest, target, lhs, to_if_expr(rhs));
1289
1290 PRECONDITION(lhs.type() == rhs.type());
1291
1292 if(lhs.type().id()==ID_array)
1293 {
1294 const exprt &a_size=to_array_type(lhs.type()).size();
1295 const auto size = numeric_cast<mp_integer>(a_size);
1296 // don't do anything, if we cannot determine the size
1297 if(!size.has_value())
1298 return target;
1299 for(mp_integer i = 0; i < *size; ++i)
1300 target=value_assignments(dest, target,
1301 index_exprt(lhs, from_integer(i, a_size.type())),
1302 index_exprt(rhs, from_integer(i, a_size.type())));
1303 }
1304 else if(lhs.type().id() == ID_pointer)
1305 return value_assignments(
1306 dest, target, dereference_exprt{lhs}, dereference_exprt{rhs});
1307 else if(lhs.type()==string_struct)
1308 return value_assignments_string_struct(dest, target, lhs, rhs);
1309 else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)
1310 {
1311 const struct_union_typet &struct_union_type=
1313
1314 for(const auto &comp : struct_union_type.components())
1315 {
1316 INVARIANT(
1317 !comp.get_name().empty(), "struct/union components must have a name");
1318
1319 target=value_assignments(dest, target,
1320 member_exprt(lhs, comp.get_name(), comp.type()),
1321 member_exprt(rhs, comp.get_name(), comp.type()));
1322 }
1323 }
1324
1325 return target;
1326}
1327
1329 goto_programt &dest,
1331 const exprt &lhs, const if_exprt &rhs)
1332{
1333 goto_programt tmp;
1334
1335 goto_programt::targett goto_else =
1337 boolean_negate(rhs.cond()), target->source_location()));
1339 true_exprt(), target->source_location()));
1340 goto_programt::targett else_target =
1341 tmp.add(goto_programt::make_skip(target->source_location()));
1342 goto_programt::targett out_target =
1343 tmp.add(goto_programt::make_skip(target->source_location()));
1344
1345 goto_else->complete_goto(else_target);
1346 goto_out->complete_goto(out_target);
1347
1348 value_assignments(tmp, goto_out, lhs, rhs.true_case());
1349 value_assignments(tmp, else_target, lhs, rhs.false_case());
1350
1351 goto_programt::targett last=target;
1352 ++last;
1353 dest.insert_before_swap(target, tmp);
1354 --last;
1355
1356 return last;
1357}
1358
1360 goto_programt &dest,
1362 const exprt &lhs, const exprt &rhs)
1363{
1364 // copy all the values
1365 goto_programt tmp;
1366
1369 member(lhs, whatt::IS_ZERO),
1370 member(rhs, whatt::IS_ZERO),
1371 target->source_location()},
1372 target->source_location()));
1373
1376 member(lhs, whatt::LENGTH),
1377 member(rhs, whatt::LENGTH),
1378 target->source_location()},
1379 target->source_location()));
1380
1383 member(lhs, whatt::SIZE),
1384 member(rhs, whatt::SIZE),
1385 target->source_location()},
1386 target->source_location()));
1387
1388 goto_programt::targett last=target;
1389 ++last;
1390 dest.insert_before_swap(target, tmp);
1391 --last;
1392
1393 return last;
1394}
1395
1397{
1398 if(a.is_nil())
1399 return a;
1400
1403 "either the expression is not a string or it is not a pointer to one");
1404
1405 exprt struct_op=
1406 a.type().id()==ID_pointer?
1408
1409 irep_idt component_name;
1410
1411 switch(what)
1412 {
1413 case whatt::IS_ZERO: component_name="is_zero"; break;
1414 case whatt::SIZE: component_name="size"; break;
1415 case whatt::LENGTH: component_name="length"; break;
1416 }
1417
1418 return member_exprt(struct_op, component_name, build_type(what));
1419}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral 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:55
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
typet c_bool_type()
Definition c_types.cpp:105
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
Array constructor from list of elements.
Definition std_expr.h:1563
Array constructor from single element.
Definition std_expr.h:1498
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:153
exprt & op0()
Definition expr.h:125
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the declaration of a local variable.
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
Data structure for representing an arbitrary statement in a program.
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:39
bool empty() const
Definition dstring.h:90
Base class for all expressions.
Definition expr.h:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:228
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
std::vector< irep_idt > parameter_identifierst
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
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.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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())
void swap(goto_programt &program)
Swap the goto program.
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:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
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:2794
const exprt & struct_op() const
Definition std_expr.h:2832
irep_idt get_component_name() const
Definition std_expr.h:2816
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:1006
exprt & op2()
Definition std_expr.h:889
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:3026
The plus expression Associativity is not specified.
Definition std_expr.h:947
const typet & base_type() const
The type of the data what we point to.
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(goto_modelt &goto_model, message_handlert &_message_handler)
Apply string abstraction to goto_model.
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)
bool build_symbol(const symbol_exprt &sym, exprt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
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
const typet & build_abstraction_type(const typet &type)
Struct constructor from list of elements.
Definition std_expr.h:1819
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:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_auxiliary
Definition symbol.h:77
bool is_macro
Definition symbol.h:62
bool is_file_local
Definition symbol.h:73
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
bool is_static_lifetime
Definition symbol.h:70
bool is_parameter
Definition symbol.h:76
bool is_thread_local
Definition symbol.h:71
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
bool is_state_var
Definition symbol.h:66
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
bool is_lvalue
Definition symbol.h:72
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:3008
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
source_locationt & add_source_location()
Definition type.h:77
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
int main()
Definition example.cpp:18
#define Forall_operands(it, expr)
Definition expr.h:27
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
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 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.
exprt pointer_offset(const exprt &pointer)
Various predicates over pointers in programs.
BigInt mp_integer
Definition smt_terms.h:18
#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:525
#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:1842
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1603
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
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 minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1031
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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: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 tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition std_types.h:434
void string_abstraction(goto_modelt &goto_model, message_handlert &message_handler)
static bool is_ptr_argument(const typet &type)
String Abstraction.
const string_constantt & to_string_constant(const exprt &expr)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175
dstringt irep_idt