cprover
string_abstraction.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String Abstraction
4 
5 Author: 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>
19 #include <util/type_eq.h>
20 
21 #include "pointer_arithmetic.h"
22 
24  const exprt &object,
25  exprt &dest, bool write)
26 {
27  // debugging
28  if(build(object, dest, write))
29  return true;
30 
31  // extra consistency check
32  // use
33  // #define build_wrap(a,b,c) build(a,b,c)
34  // to avoid it
35  const typet &a_t=build_abstraction_type(object.type());
36  /*assert(type_eq(dest.type(), a_t, ns) ||
37  (dest.type().id()==ID_array && a_t.id()==ID_pointer &&
38  type_eq(dest.type().subtype(), a_t.subtype(), ns)));
39  */
40  if(!type_eq(dest.type(), a_t, ns) &&
41  !(dest.type().id()==ID_array && a_t.id()==ID_pointer &&
42  type_eq(dest.type().subtype(), a_t.subtype(), ns)))
43  {
44  warning() << "warning: inconsistent abstract type for "
45  << object.pretty() << eom;
46  return true;
47  }
48 
49  return false;
50 }
51 
53 {
54  return type.id()==ID_pointer &&
55  type_eq(type.subtype(), string_struct, ns);
56 }
57 
58 static inline bool is_ptr_argument(const typet &type)
59 {
60  return type.id()==ID_pointer;
61 }
62 
66  goto_programt &dest)
67 {
69  string_abstraction(dest);
70 }
71 
75  goto_functionst &dest)
76 {
78  string_abstraction(dest);
79 }
80 
82  goto_modelt &goto_model,
84 {
86  goto_model.symbol_table,
88  goto_model.goto_functions);
89 }
90 
92  symbol_tablet &_symbol_table,
93  message_handlert &_message_handler):
94  messaget(_message_handler),
95  arg_suffix("#strarg"),
96  sym_suffix("#str$fcn"),
97  symbol_table(_symbol_table),
98  ns(_symbol_table),
99  temporary_counter(0)
100 {
101  struct_typet s;
102 
103  s.components().resize(3);
104 
105  s.components()[0].set_name("is_zero");
106  s.components()[0].set_pretty_name("is_zero");
107  s.components()[0].type()=build_type(whatt::IS_ZERO);
108 
109  s.components()[1].set_name("length");
110  s.components()[1].set_pretty_name("length");
111  s.components()[1].type()=build_type(whatt::LENGTH);
112 
113  s.components()[2].set_name("size");
114  s.components()[2].set_pretty_name("size");
115  s.components()[2].type()=build_type(whatt::SIZE);
116 
117  string_struct=s;
118 }
119 
121 {
122  typet type;
123 
124  switch(what)
125  {
126  case whatt::IS_ZERO: type=bool_typet(); break;
127  case whatt::LENGTH: type=size_type(); break;
128  case whatt::SIZE: type=size_type(); break;
129  }
130 
131  return type;
132 }
133 
135 {
136  Forall_goto_functions(it, dest)
137  {
138  sym_suffix="#str$"+id2string(it->first);
139  add_str_arguments(it->first, it->second);
140  abstract(it->second.body);
141  current_args.clear();
142  }
143 
144  // do we have a main?
145  goto_functionst::function_mapt::iterator
146  m_it=dest.function_map.find(dest.entry_point());
147 
148  if(m_it!=dest.function_map.end())
149  {
150  goto_programt &main=m_it->second.body;
151 
152  // do initialization
154  main.swap(initialization);
156  }
157 }
158 
160 {
161  abstract(dest);
162 
163  // do initialization
165  dest.swap(initialization);
167 }
168 
170  const irep_idt &name,
172 {
173  symbolt &fct_symbol=*symbol_table.get_writeable(name);
174 
175  code_typet::parameterst &parameters=
176  to_code_type(fct.type).parameters();
177  code_typet::parameterst str_args;
178 
179  for(code_typet::parameterst::iterator
180  it=parameters.begin();
181  it!=parameters.end();
182  ++it)
183  {
184  const typet &abstract_type=build_abstraction_type(it->type());
185  if(abstract_type.is_nil())
186  continue;
187 
188  const irep_idt &identifier=it->get_identifier();
189  if(identifier=="")
190  continue; // ignore
191 
192  add_argument(str_args, fct_symbol, abstract_type,
193  id2string(it->get_base_name())+arg_suffix,
194  id2string(identifier)+arg_suffix);
195 
196  current_args.insert(identifier);
197  }
198 
199  parameters.insert(parameters.end(), str_args.begin(), str_args.end());
200  code_typet::parameterst &symb_parameters=
201  to_code_type(fct_symbol.type).parameters();
202  symb_parameters.insert(
203  symb_parameters.end(), str_args.begin(), str_args.end());
204 }
205 
207  code_typet::parameterst &str_args,
208  const symbolt &fct_symbol,
209  const typet &type,
210  const irep_idt &base_name,
211  const irep_idt &identifier)
212 {
213  typet final_type=is_ptr_argument(type)?
214  type:pointer_type(type);
215 
216  str_args.push_back(code_typet::parametert(final_type));
217  str_args.back().add_source_location()=fct_symbol.location;
218  str_args.back().set_base_name(base_name);
219  str_args.back().set_identifier(identifier);
220 
221  auxiliary_symbolt new_symbol;
222  new_symbol.type=final_type;
223  new_symbol.value.make_nil();
224  new_symbol.location=str_args.back().source_location();
225  new_symbol.name=str_args.back().get_identifier();
226  new_symbol.module=fct_symbol.module;
227  new_symbol.base_name=str_args.back().get_base_name();
228  new_symbol.mode=fct_symbol.mode;
229  new_symbol.pretty_name=str_args.back().get_base_name();
230 
231  symbol_table.insert(std::move(new_symbol));
232 }
233 
235 {
236  locals.clear();
237 
239  it=abstract(dest, it);
240 
241  if(locals.empty())
242  return;
243 
244  // go over it again for the newly added locals
245  declare_define_locals(dest);
246  locals.clear();
247 }
248 
250 {
251  typedef std::unordered_map<irep_idt, goto_programt::targett> available_declst;
252  available_declst available_decls;
253 
255  if(it->is_decl())
256  // same name may exist several times due to inlining, make sure the first
257  // declaration is used
258  available_decls.insert(std::make_pair(
259  to_code_decl(it->code).get_identifier(), it));
260 
261  // declare (and, if necessary, define) locals
262  for(const auto &l : locals)
263  {
264  goto_programt::targett ref_instr=dest.instructions.begin();
265  bool has_decl=false;
266 
267  available_declst::const_iterator entry=available_decls.find(l.first);
268 
269  if(available_declst::const_iterator(available_decls.end())!=entry)
270  {
271  ref_instr=entry->second;
272  has_decl=true;
273  }
274 
275  goto_programt tmp;
276  make_decl_and_def(tmp, ref_instr, l.second, l.first);
277 
278  if(has_decl)
279  ++ref_instr;
280  dest.insert_before_swap(ref_instr, tmp);
281  }
282 }
283 
285  goto_programt::targett ref_instr,
286  const irep_idt &identifier,
287  const irep_idt &source_sym)
288 {
289  const symbolt &symbol=ns.lookup(identifier);
290  symbol_exprt sym_expr=symbol.symbol_expr();
291 
293  decl1->make_decl();
294  decl1->source_location=ref_instr->source_location;
295  decl1->function=ref_instr->function;
296  decl1->code=code_declt(sym_expr);
297  decl1->code.add_source_location()=ref_instr->source_location;
298 
299  exprt val=symbol.value;
300  // initialize pointers with suitable objects
301  if(val.is_nil())
302  {
303  const symbolt &orig=ns.lookup(source_sym);
304  val=make_val_or_dummy_rec(dest, ref_instr, symbol, ns.follow(orig.type));
305  }
306 
307  // may still be nil (structs, then assignments have been done already)
308  if(val.is_not_nil())
309  {
310  goto_programt::targett assignment1=dest.add_instruction();
311  assignment1->make_assignment();
312  assignment1->source_location=ref_instr->source_location;
313  assignment1->function=ref_instr->function;
314  assignment1->code=code_assignt(sym_expr, val);
315  assignment1->code.add_source_location()=ref_instr->source_location;
316  }
317 }
318 
320  goto_programt::targett ref_instr,
321  const symbolt &symbol, const typet &source_type)
322 {
323  const typet &eff_type=ns.follow(symbol.type);
324 
325  if(eff_type.id()==ID_array || eff_type.id()==ID_pointer)
326  {
327  const typet &source_subt=is_ptr_string_struct(eff_type)?
328  source_type:ns.follow(source_type.subtype());
330  dest, ref_instr, symbol, irep_idt(),
331  eff_type.subtype(), source_subt);
332 
333  if(eff_type.id()==ID_array)
334  return array_of_exprt(sym_expr, to_array_type(eff_type));
335  else
336  return address_of_exprt(sym_expr);
337  }
338  else if(eff_type.id()==ID_union ||
339  (eff_type.id()==ID_struct && !type_eq(eff_type, string_struct, ns)))
340  {
341  const struct_union_typet &su_source=to_struct_union_type(source_type);
342  const struct_union_typet::componentst &s_components=
343  su_source.components();
344  const struct_union_typet &struct_union_type=to_struct_union_type(eff_type);
345  const struct_union_typet::componentst &components=
346  struct_union_type.components();
347  unsigned seen=0;
348 
349  struct_union_typet::componentst::const_iterator it2=components.begin();
350  for(struct_union_typet::componentst::const_iterator
351  it=s_components.begin();
352  it!=s_components.end() && it2!=components.end();
353  ++it)
354  {
355  if(it->get_name()!=it2->get_name())
356  continue;
357 
358  const typet &eff_sub_type=ns.follow(it2->type());
359  if(eff_sub_type.id()==ID_pointer ||
360  eff_sub_type.id()==ID_array ||
361  eff_sub_type.id()==ID_struct ||
362  eff_sub_type.id()==ID_union)
363  {
365  dest, ref_instr, symbol, it2->get_name(),
366  it2->type(), ns.follow(it->type()));
367 
368  member_exprt member(symbol.symbol_expr(), it2->get_name(), it2->type());
369 
370  goto_programt::targett assignment1=dest.add_instruction();
371  assignment1->make_assignment();
372  assignment1->source_location=ref_instr->source_location;
373  assignment1->function=ref_instr->function;
374  assignment1->code=code_assignt(member, sym_expr);
375  assignment1->code.add_source_location()=ref_instr->source_location;
376  }
377 
378  ++seen;
379  ++it2;
380  }
381 
382  assert(components.size()==seen);
383  }
384 
385  return nil_exprt();
386 }
387 
389  goto_programt &dest,
390  goto_programt::targett ref_instr,
391  const symbolt &symbol,
392  const irep_idt &component_name,
393  const typet &type,
394  const typet &source_type)
395 {
396  std::string suffix="$strdummy";
397  if(!component_name.empty())
398  suffix="#"+id2string(component_name)+suffix;
399 
400  irep_idt dummy_identifier=id2string(symbol.name)+suffix;
401 
402  auxiliary_symbolt new_symbol;
403  new_symbol.type=type;
404  new_symbol.value.make_nil();
405  new_symbol.location=ref_instr->source_location;
406  new_symbol.name=dummy_identifier;
407  new_symbol.module=symbol.module;
408  new_symbol.base_name=id2string(symbol.base_name)+suffix;
409  new_symbol.mode=symbol.mode;
410  new_symbol.pretty_name=id2string(
411  symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+suffix;
412 
413  symbol_exprt sym_expr=new_symbol.symbol_expr();
414 
415  // make sure it is declared before the recursive call
417  decl->make_decl();
418  decl->source_location=ref_instr->source_location;
419  decl->function=ref_instr->function;
420  decl->code=code_declt(sym_expr);
421  decl->code.add_source_location()=ref_instr->source_location;
422 
423  // set the value - may be nil
424  if(source_type.id()==ID_array && is_char_type(source_type.subtype()) &&
425  type_eq(type, string_struct, ns))
426  {
427  new_symbol.value=struct_exprt(string_struct);
428  new_symbol.value.operands().resize(3);
429  new_symbol.value.op0()=build_unknown(whatt::IS_ZERO, false);
430  new_symbol.value.op1()=build_unknown(whatt::LENGTH, false);
431  new_symbol.value.op2()=to_array_type(source_type).size().id()==ID_infinity?
432  build_unknown(whatt::SIZE, false):to_array_type(source_type).size();
433  make_type(new_symbol.value.op2(), build_type(whatt::SIZE));
434  }
435  else
436  new_symbol.value=
437  make_val_or_dummy_rec(dest, ref_instr, new_symbol, source_type);
438 
439  if(new_symbol.value.is_not_nil())
440  {
441  goto_programt::targett assignment1=dest.add_instruction();
442  assignment1->make_assignment();
443  assignment1->source_location=ref_instr->source_location;
444  assignment1->function=ref_instr->function;
445  assignment1->code=code_assignt(sym_expr, new_symbol.value);
446  assignment1->code.add_source_location()=ref_instr->source_location;
447  }
448 
449  symbol_table.insert(std::move(new_symbol));
450 
451  return sym_expr;
452 }
453 
455  goto_programt &dest,
457 {
458  switch(it->type)
459  {
460  case ASSIGN:
461  it=abstract_assign(dest, it);
462  break;
463 
464  case GOTO:
465  case ASSERT:
466  case ASSUME:
467  if(has_string_macros(it->guard))
468  replace_string_macros(it->guard, false, it->source_location);
469  break;
470 
471  case FUNCTION_CALL:
472  abstract_function_call(dest, it);
473  break;
474 
475  case RETURN:
476  // use remove_returns
477  UNREACHABLE;
478  break;
479 
480  case END_FUNCTION:
481  case START_THREAD:
482  case END_THREAD:
483  case ATOMIC_BEGIN:
484  case ATOMIC_END:
485  case DECL:
486  case DEAD:
487  case CATCH:
488  case THROW:
489  case SKIP:
490  case OTHER:
491  case LOCATION:
492  break;
493 
494  case INCOMPLETE_GOTO:
495  case NO_INSTRUCTION_TYPE:
496  UNREACHABLE;
497  break;
498  }
499 
500  return it;
501 }
502 
504  goto_programt &dest,
505  goto_programt::targett target)
506 {
507  code_assignt &assign=to_code_assign(target->code);
508 
509  exprt &lhs=assign.lhs();
510  exprt &rhs=assign.rhs();
511 
512  if(has_string_macros(lhs))
513  {
514  replace_string_macros(lhs, true, target->source_location);
515  move_lhs_arithmetic(lhs, rhs);
516  }
517 
518  if(has_string_macros(rhs))
519  replace_string_macros(rhs, false, target->source_location);
520 
521  const typet &type=ns.follow(lhs.type());
522  if(type.id()==ID_pointer || type.id()==ID_array)
523  return abstract_pointer_assign(dest, target);
524  else if(is_char_type(type))
525  return abstract_char_assign(dest, target);
526 
527  return target;
528 }
529 
531  goto_programt &dest,
532  goto_programt::targett target)
533 {
534  code_function_callt &call=to_code_function_call(target->code);
535  code_function_callt::argumentst &arguments=call.arguments();
537 
538  const symbolt &fct_symbol=ns.lookup(call.function().get(ID_identifier));
539  const code_typet::parameterst &formal_params=
540  to_code_type(fct_symbol.type).parameters();
541 
542  code_function_callt::argumentst::const_iterator it1=arguments.begin();
543  for(code_typet::parameterst::const_iterator it2=formal_params.begin();
544  it2!=formal_params.end();
545  it2++, it1++)
546  {
547  const typet &abstract_type=build_abstraction_type(it2->type());
548  if(abstract_type.is_nil())
549  continue;
550 
551  if(it1==arguments.end())
552  {
553  error() << "function call: not enough arguments" << eom;
554  throw 0;
555  }
556 
557  str_args.push_back(exprt());
558  // if function takes void*, build for *it1 will fail if actual parameter
559  // is of some other pointer type; then just introduce an unknown
560  if(build_wrap(*it1, 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  assert(type_eq(str_args.back().type().subtype(),
567  abstract_type.subtype(), ns));
568 
569  index_exprt idx(str_args.back(), from_integer(0, index_type()));
570  // disable bounds check on that one
571  idx.set("bounds_check", false);
572 
573  str_args.back()=address_of_exprt(idx);
574  }
575 
576  if(!is_ptr_argument(abstract_type))
577  str_args.back()=address_of_exprt(str_args.back());
578  }
579 
580  arguments.insert(arguments.end(), str_args.begin(), str_args.end());
581 }
582 
584 {
585  if(expr.id()=="is_zero_string" ||
586  expr.id()=="zero_string_length" ||
587  expr.id()=="buffer_size")
588  return true;
589 
590  forall_operands(it, expr)
591  if(has_string_macros(*it))
592  return true;
593 
594  return false;
595 }
596 
598  exprt &expr,
599  bool lhs,
600  const source_locationt &source_location)
601 {
602  if(expr.id()=="is_zero_string")
603  {
604  assert(expr.operands().size()==1);
605  exprt tmp=build(expr.op0(), whatt::IS_ZERO, lhs, source_location);
606  expr.swap(tmp);
607  }
608  else if(expr.id()=="zero_string_length")
609  {
610  assert(expr.operands().size()==1);
611  exprt tmp=build(expr.op0(), whatt::LENGTH, lhs, source_location);
612  expr.swap(tmp);
613  }
614  else if(expr.id()=="buffer_size")
615  {
616  assert(expr.operands().size()==1);
617  exprt tmp=build(expr.op0(), whatt::SIZE, false, source_location);
618  expr.swap(tmp);
619  }
620  else
621  Forall_operands(it, expr)
622  replace_string_macros(*it, lhs, source_location);
623 }
624 
626  const exprt &pointer,
627  whatt what,
628  bool write,
629  const source_locationt &source_location)
630 {
631  // take care of pointer typecasts now
632  if(pointer.id()==ID_typecast)
633  {
634  // cast from another pointer type?
635  assert(pointer.operands().size()==1);
636  if(pointer.op0().type().id()!=ID_pointer)
637  return build_unknown(what, write);
638 
639  // recursive call
640  return build(pointer.op0(), what, write, source_location);
641  }
642 
643  exprt str_struct;
644  if(build_wrap(pointer, str_struct, write))
645  UNREACHABLE;
646 
647  exprt result=member(str_struct, what);
648 
649  if(what==whatt::LENGTH || what==whatt::SIZE)
650  {
651  // adjust for offset
653  result.op0().make_typecast(result.op1().type());
654  }
655 
656  return result;
657 }
658 
660 {
661  const typet &eff_type=ns.follow(type);
662  abstraction_types_mapt::const_iterator map_entry=
663  abstraction_types_map.find(eff_type);
664  if(map_entry!=abstraction_types_map.end())
665  return map_entry->second;
666 
668  tmp.swap(abstraction_types_map);
669  build_abstraction_type_rec(eff_type, tmp);
670 
671  abstraction_types_map.swap(tmp);
672  map_entry=tmp.find(eff_type);
673  assert(map_entry!=tmp.end());
674  return abstraction_types_map.insert(
675  std::make_pair(eff_type, map_entry->second)).first->second;
676 }
677 
679  const abstraction_types_mapt &known)
680 {
681  const typet &eff_type=ns.follow(type);
682  abstraction_types_mapt::const_iterator known_entry=known.find(eff_type);
683  if(known_entry!=known.end())
684  return known_entry->second;
685 
686  ::std::pair< abstraction_types_mapt::iterator, bool > map_entry(
687  abstraction_types_map.insert(::std::make_pair(
688  eff_type, nil_typet())));
689  if(!map_entry.second)
690  return map_entry.first->second;
691 
692  if(eff_type.id()==ID_array || eff_type.id()==ID_pointer)
693  {
694  // char* or void* or char[]
695  if(is_char_type(eff_type.subtype()) ||
696  eff_type.subtype().id()==ID_empty)
697  map_entry.first->second=pointer_type(string_struct);
698  else
699  {
700  const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known);
701  if(!subt.is_nil())
702  {
703  if(eff_type.id()==ID_array)
704  map_entry.first->second=
705  array_typet(subt, to_array_type(eff_type).size());
706  else
707  map_entry.first->second=pointer_type(subt);
708  }
709  }
710  }
711  else if(eff_type.id()==ID_struct || eff_type.id()==ID_union)
712  {
713  const struct_union_typet &struct_union_type=to_struct_union_type(eff_type);
714 
716  for(const auto &comp : struct_union_type.components())
717  {
718  if(comp.get_anonymous())
719  continue;
720  typet subt=build_abstraction_type_rec(comp.type(), known);
721  if(subt.is_nil())
722  // also precludes structs with pointers to the same datatype
723  continue;
724 
725  new_comp.push_back(struct_union_typet::componentt());
726  new_comp.back().set_name(comp.get_name());
727  new_comp.back().set_pretty_name(comp.get_pretty_name());
728  new_comp.back().type()=subt;
729  }
730  if(!new_comp.empty())
731  {
732  struct_union_typet t(eff_type.id());
733  t.components().swap(new_comp);
734  map_entry.first->second=t;
735  }
736  }
737 
738  return map_entry.first->second;
739 }
740 
741 bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
742 {
743  const typet &abstract_type=build_abstraction_type(object.type());
744  if(abstract_type.is_nil())
745  return true;
746 
747  if(object.id()==ID_typecast)
748  {
749  if(build(to_typecast_expr(object).op(), dest, write))
750  return true;
751 
752  return !(type_eq(dest.type(), abstract_type, ns) ||
753  (dest.type().id()==ID_array &&
754  abstract_type.id()==ID_pointer &&
755  type_eq(dest.type().subtype(), abstract_type.subtype(), ns)));
756  }
757 
758  if(object.id()==ID_string_constant)
759  {
760  const std::string &str_value = id2string(object.get(ID_value));
761  // make sure we handle the case of a string constant with string-terminating
762  // \0 in it
763  const std::size_t str_len =
764  std::min(str_value.size(), str_value.find('\0'));
765  return build_symbol_constant(str_len, str_len+1, dest);
766  }
767 
768  if(object.id()==ID_array && is_char_type(object.type().subtype()))
769  return build_array(to_array_expr(object), dest, write);
770 
771  // other constants aren't useful
772  if(object.is_constant())
773  return true;
774 
775  if(object.id()==ID_symbol)
776  return build_symbol(to_symbol_expr(object), dest);
777 
778  if(object.id()==ID_if)
779  return build_if(to_if_expr(object), dest, write);
780 
781  if(object.id()==ID_member)
782  {
783  const member_exprt &o_mem=to_member_expr(object);
784  dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type);
785  return build_wrap(o_mem.struct_op(), dest.op0(), write);
786  }
787 
788  if(object.id()==ID_dereference)
789  {
790  const dereference_exprt &o_deref=to_dereference_expr(object);
791  dest=dereference_exprt(exprt(), abstract_type);
792  return build_wrap(o_deref.pointer(), dest.op0(), write);
793  }
794 
795  if(object.id()==ID_index)
796  {
797  const index_exprt &o_index=to_index_expr(object);
798  dest=index_exprt(exprt(), o_index.index(), abstract_type);
799  return build_wrap(o_index.array(), dest.op0(), write);
800  }
801 
802  // handle pointer stuff
803  if(object.type().id()==ID_pointer)
804  return build_pointer(object, dest, write);
805 
806  return true;
807 }
808 
810  exprt &dest, bool write)
811 {
812  if_exprt new_if(o_if.cond(), exprt(), exprt());
813 
814  // recursive calls
815  bool op1_err=build_wrap(o_if.true_case(), new_if.true_case(), write);
816  bool op2_err=build_wrap(o_if.false_case(), new_if.false_case(), write);
817  if(op1_err && op2_err)
818  return true;
819  // at least one of them gave proper results
820  if(op1_err)
821  {
822  new_if.type()=new_if.false_case().type();
823  new_if.true_case()=build_unknown(new_if.type(), write);
824  }
825  else if(op2_err)
826  {
827  new_if.type()=new_if.true_case().type();
828  new_if.false_case()=build_unknown(new_if.type(), write);
829  }
830  else
831  new_if.type()=new_if.true_case().type();
832 
833  dest.swap(new_if);
834  return false;
835 }
836 
838  exprt &dest, bool write)
839 {
840  assert(is_char_type(object.type().subtype()));
841 
842  // writing is invalid
843  if(write)
844  return true;
845 
846  const exprt &a_size=to_array_type(object.type()).size();
847  mp_integer size;
848  // don't do anything, if we cannot determine the size
849  if(to_integer(a_size, size))
850  return true;
851  assert(size==object.operands().size());
852 
853  exprt::operandst::const_iterator it=object.operands().begin();
854  for(mp_integer i=0; i<size; ++i, ++it)
855  if(it->is_zero())
856  return build_symbol_constant(i, size, dest);
857 
858  return true;
859 }
860 
862  exprt &dest, bool write)
863 {
864  assert(object.type().id()==ID_pointer);
865 
866  pointer_arithmetict ptr(object);
867  if(ptr.pointer.id()==ID_address_of)
868  {
870 
871  if(a.object().id()==ID_index)
872  return build_wrap(to_index_expr(a.object()).array(), dest, write);
873 
874  // writing is invalid
875  if(write)
876  return true;
877 
878  if(build_wrap(a.object(), dest, write))
879  return true;
880  dest=address_of_exprt(dest);
881  return false;
882  }
883  else if(ptr.pointer.id()==ID_symbol &&
884  is_char_type(object.type().subtype()))
885  // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
886  // checks
887  return build_wrap(ptr.pointer, dest, write);
888 
889  // we don't handle other pointer arithmetic
890  return true;
891 }
892 
894 {
895  typet type=build_type(what);
896 
897  if(write)
898  return exprt(ID_null_object, type);
899 
900  exprt result;
901 
902  switch(what)
903  {
904  case whatt::IS_ZERO:
906  break;
907 
908  case whatt::LENGTH:
909  case whatt::SIZE:
911  break;
912  }
913 
914  return result;
915 }
916 
918 {
919  if(write)
920  return exprt(ID_null_object, type);
921 
922  // create an uninitialized dummy symbol
923  // because of a lack of contextual information we can't build a nice name
924  // here, but moving that into locals should suffice for proper operation
925  irep_idt identifier=
926  "$tmp::nondet_str#str$"+std::to_string(++temporary_counter);
927  // ensure decl and initialization
928  locals[identifier]=identifier;
929 
930  auxiliary_symbolt new_symbol;
931  new_symbol.type=type;
932  new_symbol.value.make_nil();
933  new_symbol.name=identifier;
934  new_symbol.module="$tmp";
935  new_symbol.base_name=identifier;
936  new_symbol.mode=ID_C;
937  new_symbol.pretty_name=identifier;
938 
939  symbol_table.insert(std::move(new_symbol));
940 
941  return ns.lookup(identifier).symbol_expr();
942 }
943 
945 {
946  const symbolt &symbol=ns.lookup(sym.get_identifier());
947 
948  const typet &abstract_type=build_abstraction_type(symbol.type);
949  assert(!abstract_type.is_nil());
950 
951  irep_idt identifier="";
952 
953  if(current_args.find(symbol.name)!=current_args.end())
954  identifier=id2string(symbol.name)+arg_suffix;
955  else
956  {
957  identifier=id2string(symbol.name)+sym_suffix;
958  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
959  build_new_symbol(symbol, identifier, abstract_type);
960  }
961 
962  const symbolt &str_symbol=ns.lookup(identifier);
963  dest=str_symbol.symbol_expr();
964  if(current_args.find(symbol.name)!=current_args.end() &&
965  !is_ptr_argument(abstract_type))
966  dest=dereference_exprt(dest, dest.type().subtype());
967 
968  return false;
969 }
970 
972  const irep_idt &identifier, const typet &type)
973 {
974  if(!symbol.is_static_lifetime)
975  locals[symbol.name]=identifier;
976 
977  auxiliary_symbolt new_symbol;
978  new_symbol.type=type;
979  new_symbol.value.make_nil();
980  new_symbol.location=symbol.location;
981  new_symbol.name=identifier;
982  new_symbol.module=symbol.module;
983  new_symbol.base_name=id2string(symbol.base_name)+sym_suffix;
984  new_symbol.mode=symbol.mode;
985  new_symbol.pretty_name=
986  id2string(symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+
987  sym_suffix;
988  new_symbol.is_static_lifetime=symbol.is_static_lifetime;
989  new_symbol.is_thread_local=symbol.is_thread_local;
990 
991  symbol_table.insert(std::move(new_symbol));
992 
993  if(symbol.is_static_lifetime)
994  {
996  dummy_loc->source_location=symbol.location;
997  make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
998  initialization.instructions.erase(dummy_loc);
999  }
1000 }
1001 
1003  const mp_integer &zero_length,
1004  const mp_integer &buf_size,
1005  exprt &dest)
1006 {
1007  irep_idt base="$string_constant_str_"+integer2string(zero_length)
1008  +"_"+integer2string(buf_size);
1009  irep_idt identifier="string_abstraction::"+id2string(base);
1010 
1011  if(symbol_table.symbols.find(identifier)==
1012  symbol_table.symbols.end())
1013  {
1014  auxiliary_symbolt new_symbol;
1015  new_symbol.type=string_struct;
1016  new_symbol.value.make_nil();
1017  new_symbol.name=identifier;
1018  new_symbol.base_name=base;
1019  new_symbol.mode=ID_C;
1020  new_symbol.pretty_name=base;
1021  new_symbol.is_static_lifetime=true;
1022  new_symbol.is_thread_local=false;
1023  new_symbol.is_file_local=false;
1024 
1025  {
1026  struct_exprt value(string_struct);
1027  value.operands().resize(3);
1028 
1029  value.op0()=true_exprt();
1030  value.op1()=from_integer(zero_length, build_type(whatt::LENGTH));
1031  value.op2()=from_integer(buf_size, build_type(whatt::SIZE));
1032 
1033  // initialization
1035  assignment1->make_assignment();
1036  assignment1->code=code_assignt(new_symbol.symbol_expr(), value);
1037  }
1038 
1039  symbol_table.insert(std::move(new_symbol));
1040  }
1041 
1042  dest=address_of_exprt(symbol_exprt(identifier, string_struct));
1043 
1044  return false;
1045 }
1046 
1048 {
1049  if(lhs.id()==ID_minus)
1050  {
1051  // move op1 to rhs
1052  exprt rest=lhs.op0();
1053  rhs=plus_exprt(rhs, lhs.op1());
1054  rhs.type()=lhs.type();
1055  lhs=rest;
1056  }
1057 }
1058 
1060  goto_programt &dest,
1061  goto_programt::targett target)
1062 {
1063  code_assignt &assign=to_code_assign(target->code);
1064 
1065  exprt &lhs=assign.lhs();
1066  exprt rhs=assign.rhs();
1067  exprt *rhsp=&(assign.rhs());
1068 
1069  while(rhsp->id()==ID_typecast)
1070  rhsp=&(rhsp->op0());
1071 
1072  const typet &abstract_type=build_abstraction_type(lhs.type());
1073  if(abstract_type.is_nil())
1074  return target;
1075 
1076  exprt new_lhs, new_rhs;
1077  if(build_wrap(lhs, new_lhs, true))
1078  return target;
1079 
1080  bool unknown=(abstract_type!=build_abstraction_type(rhsp->type()) ||
1081  build_wrap(rhs, new_rhs, false));
1082  if(unknown)
1083  new_rhs=build_unknown(abstract_type, false);
1084 
1085  if(lhs.type().id()==ID_pointer && !unknown)
1086  {
1087  goto_programt::instructiont assignment;
1088  assignment.make_assignment();
1089  assignment.source_location=target->source_location;
1090  assignment.function=target->function;
1091  assignment.code=code_assignt(new_lhs, new_rhs);
1092  assignment.code.add_source_location()=target->source_location;
1093  dest.insert_before_swap(target, assignment);
1094  ++target;
1095 
1096  return target;
1097  }
1098  else
1099  {
1100  return value_assignments(dest, target, new_lhs, new_rhs);
1101  }
1102 }
1103 
1105  goto_programt &dest,
1106  goto_programt::targett target)
1107 {
1108  code_assignt &assign=to_code_assign(target->code);
1109 
1110  exprt &lhs=assign.lhs();
1111  exprt *rhsp=&(assign.rhs());
1112 
1113  while(rhsp->id()==ID_typecast)
1114  rhsp=&(rhsp->op0());
1115 
1116  // we only care if the constant zero is assigned
1117  if(!rhsp->is_zero())
1118  return target;
1119 
1120  // index into a character array
1121  if(lhs.id()==ID_index)
1122  {
1123  const index_exprt &i_lhs=to_index_expr(lhs);
1124 
1125  exprt new_lhs;
1126  if(!build_wrap(i_lhs.array(), new_lhs, true))
1127  {
1128  exprt i2=member(new_lhs, whatt::LENGTH);
1129  assert(i2.is_not_nil());
1130 
1131  exprt new_length=i_lhs.index();
1132  make_type(new_length, i2.type());
1133 
1134  if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
1135  new_length, i2);
1136 
1137  return char_assign(dest, target, new_lhs, i2, min_expr);
1138  }
1139  }
1140  else if(lhs.id()==ID_dereference)
1141  {
1142  pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
1143  exprt new_lhs;
1144  if(!build_wrap(ptr.pointer, new_lhs, true))
1145  {
1146  const exprt i2=member(new_lhs, whatt::LENGTH);
1147  assert(i2.is_not_nil());
1148 
1150  return
1151  char_assign(
1152  dest,
1153  target,
1154  new_lhs,
1155  i2,
1156  ptr.offset.is_nil()?
1158  ptr.offset);
1159  }
1160  }
1161 
1162  return target;
1163 }
1164 
1166  goto_programt &dest,
1167  goto_programt::targett target,
1168  const exprt &new_lhs,
1169  const exprt &lhs,
1170  const exprt &rhs)
1171 {
1172  goto_programt tmp;
1173 
1174  const exprt i1=member(new_lhs, whatt::IS_ZERO);
1175  assert(i1.is_not_nil());
1176 
1177  goto_programt::targett assignment1=tmp.add_instruction();
1178  assignment1->make_assignment();
1179  assignment1->source_location=target->source_location;
1180  assignment1->function=target->function;
1181  assignment1->code=code_assignt(i1, true_exprt());
1182  assignment1->code.add_source_location()=target->source_location;
1183 
1184  goto_programt::targett assignment2=tmp.add_instruction();
1185  assignment2->make_assignment();
1186  assignment2->source_location=target->source_location;
1187  assignment2->function=target->function;
1188  assignment2->code=code_assignt(lhs, rhs);
1189  assignment2->code.add_source_location()=target->source_location;
1190 
1192  assignment2->code.op0(),
1193  assignment2->code.op1());
1194 
1195  dest.insert_before_swap(target, tmp);
1196  ++target;
1197  ++target;
1198 
1199  return target;
1200 }
1201 
1203  goto_programt &dest,
1204  goto_programt::targett target,
1205  const exprt &lhs,
1206  const exprt &rhs)
1207 {
1208  if(rhs.id()==ID_if)
1209  return value_assignments_if(dest, target, lhs, to_if_expr(rhs));
1210 
1211  assert(type_eq(lhs.type(), rhs.type(), ns));
1212 
1213  if(lhs.type().id()==ID_array)
1214  {
1215  const exprt &a_size=to_array_type(lhs.type()).size();
1216  mp_integer size;
1217  // don't do anything, if we cannot determine the size
1218  if(to_integer(a_size, size))
1219  return target;
1220  for(mp_integer i=0; i<size; ++i)
1221  target=value_assignments(dest, target,
1222  index_exprt(lhs, from_integer(i, a_size.type())),
1223  index_exprt(rhs, from_integer(i, a_size.type())));
1224  }
1225  else if(lhs.type().id()==ID_pointer)
1226  return value_assignments(dest, target,
1227  dereference_exprt(lhs, lhs.type().subtype()),
1228  dereference_exprt(rhs, rhs.type().subtype()));
1229  else if(lhs.type()==string_struct)
1230  return value_assignments_string_struct(dest, target, lhs, rhs);
1231  else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)
1232  {
1233  const struct_union_typet &struct_union_type=
1234  to_struct_union_type(lhs.type());
1235 
1236  for(const auto &comp : struct_union_type.components())
1237  {
1238  assert(!comp.get_name().empty());
1239 
1240  target=value_assignments(dest, target,
1241  member_exprt(lhs, comp.get_name(), comp.type()),
1242  member_exprt(rhs, comp.get_name(), comp.type()));
1243  }
1244  }
1245 
1246  return target;
1247 }
1248 
1250  goto_programt &dest,
1251  goto_programt::targett target,
1252  const exprt &lhs, const if_exprt &rhs)
1253 {
1254  goto_programt tmp;
1255 
1258  goto_programt::targett else_target=tmp.add_instruction(SKIP);
1260 
1261  goto_else->function=target->function;
1262  goto_else->source_location=target->source_location;
1263  goto_else->make_goto(else_target, rhs.cond());
1264  goto_else->guard.make_not();
1265 
1266  goto_out->function=target->function;
1267  goto_out->source_location=target->source_location;
1268  goto_out->make_goto(out_target, true_exprt());
1269 
1270  else_target->function=target->function;
1271  else_target->source_location=target->source_location;
1272 
1273  out_target->function=target->function;
1274  out_target->source_location=target->source_location;
1275 
1276  value_assignments(tmp, goto_out, lhs, rhs.true_case());
1277  value_assignments(tmp, else_target, lhs, rhs.false_case());
1278 
1279  goto_programt::targett last=target;
1280  ++last;
1281  dest.insert_before_swap(target, tmp);
1282  --last;
1283 
1284  return last;
1285 }
1286 
1288  goto_programt &dest,
1289  goto_programt::targett target,
1290  const exprt &lhs, const exprt &rhs)
1291 {
1292  // copy all the values
1293  goto_programt tmp;
1294 
1295  {
1297  assignment->code=code_assignt(
1298  member(lhs, whatt::IS_ZERO),
1299  member(rhs, whatt::IS_ZERO));
1300  assignment->code.add_source_location()=target->source_location;
1301  assignment->function=target->function;
1302  assignment->source_location=target->source_location;
1303  }
1304 
1305  {
1307  assignment->code=code_assignt(
1308  member(lhs, whatt::LENGTH),
1309  member(rhs, whatt::LENGTH));
1310  assignment->code.add_source_location()=target->source_location;
1311  assignment->function=target->function;
1312  assignment->source_location=target->source_location;
1313  }
1314 
1315  {
1317  assignment->code=code_assignt(
1318  member(lhs, whatt::SIZE),
1319  member(rhs, whatt::SIZE));
1320  assignment->code.add_source_location()=target->source_location;
1321  assignment->function=target->function;
1322  assignment->source_location=target->source_location;
1323  }
1324 
1325  goto_programt::targett last=target;
1326  ++last;
1327  dest.insert_before_swap(target, tmp);
1328  --last;
1329 
1330  return last;
1331 }
1332 
1334 {
1335  if(a.is_nil())
1336  return a;
1337 
1338  assert(type_eq(a.type(), string_struct, ns) ||
1339  is_ptr_string_struct(a.type()));
1340 
1341  exprt struct_op=
1342  a.type().id()==ID_pointer?
1344 
1345  irep_idt component_name;
1346 
1347  switch(what)
1348  {
1349  case whatt::IS_ZERO: component_name="is_zero"; break;
1350  case whatt::SIZE: component_name="size"; break;
1351  case whatt::LENGTH: component_name="length"; break;
1352  }
1353 
1354  member_exprt result(struct_op, component_name, build_type(what));
1355 
1356  return result;
1357 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: type_eq.cpp:18
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
The type of an expression.
Definition: type.h:22
bool build_array(const array_exprt &object, exprt &dest, bool write)
irep_idt name
The unique identifier.
Definition: symbol.h:43
const std::string arg_suffix
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
exprt & true_case()
Definition: std_expr.h:3395
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
bool is_thread_local
Definition: symbol.h:67
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt & object()
Definition: std_expr.h:3180
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
void make_type(exprt &dest, const typet &type)
exprt & op0()
Definition: expr.h:72
exprt build_unknown(whatt what, bool write)
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
irep_idt mode
Language mode.
Definition: symbol.h:52
goto_programt initialization
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
Definition: std_expr.h:1640
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
void declare_define_locals(goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::vector< componentt > componentst
Definition: std_types.h:243
std::vector< parametert > parameterst
Definition: std_types.h:767
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
bool build_wrap(const exprt &object, exprt &dest, bool write)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
static typet build_type(whatt what)
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
typet & type()
Definition: expr.h:56
void add_str_arguments(const irep_idt &name, goto_functionst::goto_functiont &fct)
exprt::operandst argumentst
Definition: std_code.h:858
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3201
The proper Booleans.
Definition: std_types.h:34
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
bool is_static_lifetime
Definition: symbol.h:67
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
Extract member of struct or union.
Definition: std_expr.h:3871
void add_argument(code_typet::parameterst &str_args, const symbolt &fct_symbol, const typet &type, const irep_idt &base_name, const irep_idt &identifier)
mstreamt & warning() const
Definition: message.h:307
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:87
void clear()
Clear the goto program.
Definition: goto_program.h:611
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
::std::set< irep_idt > current_args
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
exprt & lhs()
Definition: std_code.h:208
bool build_symbol(const symbol_exprt &sym, exprt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
The boolean constant true.
Definition: std_expr.h:4488
argumentst & arguments()
Definition: std_code.h:860
bool is_char_type(const typet &type) const
static bool is_ptr_argument(const typet &type)
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:253
::std::map< typet, typet > abstraction_types_mapt
String Abstraction.
The NIL expression.
Definition: std_expr.h:4510
exprt & rhs()
Definition: std_code.h:213
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
Operator to dereference a pointer.
Definition: std_expr.h:3284
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
const irep_idt & get_identifier() const
Definition: std_code.cpp:14
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
exprt & op1()
Definition: expr.h:75
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
mstreamt & error() const
Definition: message.h:302
::goto_functiont goto_functiont
symbol_tablet & symbol_table
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
int main()
const exprt & size() const
Definition: std_types.h:1014
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
array constructor from single element
Definition: std_expr.h:1550
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
goto_programt::targett abstract(goto_programt &dest, goto_programt::targett it)
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
Operator to return the address of an object.
Definition: std_expr.h:3170
exprt & false_case()
Definition: std_expr.h:3405
const symbolst & symbols
Various predicates over pointers in programs.
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
The boolean constant false.
Definition: std_expr.h:4499
const typet & build_abstraction_type(const typet &type)
void abstract_function_call(goto_programt &dest, goto_programt::targett it)
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:605
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
void operator()(goto_programt &dest)
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
static irep_idt entry_point()
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
mstreamt & result() const
Definition: message.h:312
exprt & index()
Definition: std_expr.h:1496
exprt & function()
Definition: std_code.h:848
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3307
const exprt & struct_op() const
Definition: std_expr.h:3911
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
exprt pointer_offset(const exprt &pointer)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:125
irep_idt get_component_name() const
Definition: std_expr.h:3895
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)
#define UNREACHABLE
Definition: invariant.h:250
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
bool is_file_local
Definition: symbol.h:68
The NIL type.
Definition: std_types.h:44
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:161
source_locationt & add_source_location()
Definition: expr.h:130
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
bool build_pointer(const exprt &object, exprt &dest, bool write)
arrays with given size
Definition: std_types.h:1004
binary minus
Definition: std_expr.h:959
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
bool is_ptr_string_struct(const typet &type) const
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
dstringt irep_idt
Definition: irep.h:31
const typet & subtype() const
Definition: type.h:33
static bool has_string_macros(const exprt &expr)
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1815
exprt member(const exprt &a, whatt what)
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1486
abstraction_types_mapt abstraction_types_map
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
array constructor from list of elements
Definition: std_expr.h:1617
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
array index operator
Definition: std_expr.h:1462