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:
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::targett target)
532 {
533  code_function_callt &call=to_code_function_call(target->code);
534  code_function_callt::argumentst &arguments=call.arguments();
536 
537  const symbolt &fct_symbol=ns.lookup(call.function().get(ID_identifier));
538  const code_typet::parameterst &formal_params=
539  to_code_type(fct_symbol.type).parameters();
540 
541  code_function_callt::argumentst::const_iterator it1=arguments.begin();
542  for(code_typet::parameterst::const_iterator it2=formal_params.begin();
543  it2!=formal_params.end();
544  it2++, it1++)
545  {
546  const typet &abstract_type=build_abstraction_type(it2->type());
547  if(abstract_type.is_nil())
548  continue;
549 
550  if(it1==arguments.end())
551  {
552  error() << "function call: not enough arguments" << eom;
553  throw 0;
554  }
555 
556  str_args.push_back(exprt());
557  // if function takes void*, build for *it1 will fail if actual parameter
558  // is of some other pointer type; then just introduce an unknown
559  if(build_wrap(*it1, str_args.back(), false))
560  str_args.back()=build_unknown(abstract_type, false);
561  // array -> pointer translation
562  if(str_args.back().type().id()==ID_array &&
563  abstract_type.id()==ID_pointer)
564  {
565  assert(type_eq(str_args.back().type().subtype(),
566  abstract_type.subtype(), ns));
567 
568  index_exprt idx(str_args.back(), from_integer(0, index_type()));
569  // disable bounds check on that one
570  idx.set("bounds_check", false);
571 
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  arguments.insert(arguments.end(), str_args.begin(), str_args.end());
580 }
581 
583 {
584  if(expr.id()=="is_zero_string" ||
585  expr.id()=="zero_string_length" ||
586  expr.id()=="buffer_size")
587  return true;
588 
589  forall_operands(it, expr)
590  if(has_string_macros(*it))
591  return true;
592 
593  return false;
594 }
595 
597  exprt &expr,
598  bool lhs,
599  const source_locationt &source_location)
600 {
601  if(expr.id()=="is_zero_string")
602  {
603  assert(expr.operands().size()==1);
604  exprt tmp=build(expr.op0(), whatt::IS_ZERO, lhs, source_location);
605  expr.swap(tmp);
606  }
607  else if(expr.id()=="zero_string_length")
608  {
609  assert(expr.operands().size()==1);
610  exprt tmp=build(expr.op0(), whatt::LENGTH, lhs, source_location);
611  expr.swap(tmp);
612  }
613  else if(expr.id()=="buffer_size")
614  {
615  assert(expr.operands().size()==1);
616  exprt tmp=build(expr.op0(), whatt::SIZE, false, source_location);
617  expr.swap(tmp);
618  }
619  else
620  Forall_operands(it, expr)
621  replace_string_macros(*it, lhs, source_location);
622 }
623 
625  const exprt &pointer,
626  whatt what,
627  bool write,
628  const source_locationt &source_location)
629 {
630  // take care of pointer typecasts now
631  if(pointer.id()==ID_typecast)
632  {
633  // cast from another pointer type?
634  assert(pointer.operands().size()==1);
635  if(pointer.op0().type().id()!=ID_pointer)
636  return build_unknown(what, write);
637 
638  // recursive call
639  return build(pointer.op0(), what, write, source_location);
640  }
641 
642  exprt str_struct;
643  if(build_wrap(pointer, str_struct, write))
644  UNREACHABLE;
645 
646  exprt result=member(str_struct, what);
647 
648  if(what==whatt::LENGTH || what==whatt::SIZE)
649  {
650  // adjust for offset
652  result.op0().make_typecast(result.op1().type());
653  }
654 
655  return result;
656 }
657 
659 {
660  const typet &eff_type=ns.follow(type);
661  abstraction_types_mapt::const_iterator map_entry=
662  abstraction_types_map.find(eff_type);
663  if(map_entry!=abstraction_types_map.end())
664  return map_entry->second;
665 
667  tmp.swap(abstraction_types_map);
668  build_abstraction_type_rec(eff_type, tmp);
669 
670  abstraction_types_map.swap(tmp);
671  map_entry=tmp.find(eff_type);
672  assert(map_entry!=tmp.end());
673  return abstraction_types_map.insert(
674  std::make_pair(eff_type, map_entry->second)).first->second;
675 }
676 
678  const abstraction_types_mapt &known)
679 {
680  const typet &eff_type=ns.follow(type);
681  abstraction_types_mapt::const_iterator known_entry=known.find(eff_type);
682  if(known_entry!=known.end())
683  return known_entry->second;
684 
685  ::std::pair< abstraction_types_mapt::iterator, bool > map_entry(
686  abstraction_types_map.insert(::std::make_pair(
687  eff_type, nil_typet())));
688  if(!map_entry.second)
689  return map_entry.first->second;
690 
691  if(eff_type.id()==ID_array || eff_type.id()==ID_pointer)
692  {
693  // char* or void* or char[]
694  if(is_char_type(eff_type.subtype()) ||
695  eff_type.subtype().id()==ID_empty)
696  map_entry.first->second=pointer_type(string_struct);
697  else
698  {
699  const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known);
700  if(!subt.is_nil())
701  {
702  if(eff_type.id()==ID_array)
703  map_entry.first->second=
704  array_typet(subt, to_array_type(eff_type).size());
705  else
706  map_entry.first->second=pointer_type(subt);
707  }
708  }
709  }
710  else if(eff_type.id()==ID_struct || eff_type.id()==ID_union)
711  {
712  const struct_union_typet &struct_union_type=to_struct_union_type(eff_type);
713 
715  for(const auto &comp : struct_union_type.components())
716  {
717  if(comp.get_anonymous())
718  continue;
719  typet subt=build_abstraction_type_rec(comp.type(), known);
720  if(subt.is_nil())
721  // also precludes structs with pointers to the same datatype
722  continue;
723 
724  new_comp.push_back(struct_union_typet::componentt());
725  new_comp.back().set_name(comp.get_name());
726  new_comp.back().set_pretty_name(comp.get_pretty_name());
727  new_comp.back().type()=subt;
728  }
729  if(!new_comp.empty())
730  {
731  struct_union_typet t(eff_type.id());
732  t.components().swap(new_comp);
733  map_entry.first->second=t;
734  }
735  }
736 
737  return map_entry.first->second;
738 }
739 
740 bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
741 {
742  const typet &abstract_type=build_abstraction_type(object.type());
743  if(abstract_type.is_nil())
744  return true;
745 
746  if(object.id()==ID_typecast)
747  {
748  if(build(to_typecast_expr(object).op(), dest, write))
749  return true;
750 
751  return !(type_eq(dest.type(), abstract_type, ns) ||
752  (dest.type().id()==ID_array &&
753  abstract_type.id()==ID_pointer &&
754  type_eq(dest.type().subtype(), abstract_type.subtype(), ns)));
755  }
756 
757  if(object.id()==ID_string_constant)
758  {
759  const std::string &str_value = id2string(object.get(ID_value));
760  // make sure we handle the case of a string constant with string-terminating
761  // \0 in it
762  const std::size_t str_len =
763  std::min(str_value.size(), str_value.find('\0'));
764  return build_symbol_constant(str_len, str_len+1, dest);
765  }
766 
767  if(object.id()==ID_array && is_char_type(object.type().subtype()))
768  return build_array(to_array_expr(object), dest, write);
769 
770  // other constants aren't useful
771  if(object.is_constant())
772  return true;
773 
774  if(object.id()==ID_symbol)
775  return build_symbol(to_symbol_expr(object), dest);
776 
777  if(object.id()==ID_if)
778  return build_if(to_if_expr(object), dest, write);
779 
780  if(object.id()==ID_member)
781  {
782  const member_exprt &o_mem=to_member_expr(object);
783  dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type);
784  return build_wrap(o_mem.struct_op(), dest.op0(), write);
785  }
786 
787  if(object.id()==ID_dereference)
788  {
789  const dereference_exprt &o_deref=to_dereference_expr(object);
790  dest=dereference_exprt(exprt(), abstract_type);
791  return build_wrap(o_deref.pointer(), dest.op0(), write);
792  }
793 
794  if(object.id()==ID_index)
795  {
796  const index_exprt &o_index=to_index_expr(object);
797  dest=index_exprt(exprt(), o_index.index(), abstract_type);
798  return build_wrap(o_index.array(), dest.op0(), write);
799  }
800 
801  // handle pointer stuff
802  if(object.type().id()==ID_pointer)
803  return build_pointer(object, dest, write);
804 
805  return true;
806 }
807 
809  exprt &dest, bool write)
810 {
811  if_exprt new_if(o_if.cond(), exprt(), exprt());
812 
813  // recursive calls
814  bool op1_err=build_wrap(o_if.true_case(), new_if.true_case(), write);
815  bool op2_err=build_wrap(o_if.false_case(), new_if.false_case(), write);
816  if(op1_err && op2_err)
817  return true;
818  // at least one of them gave proper results
819  if(op1_err)
820  {
821  new_if.type()=new_if.false_case().type();
822  new_if.true_case()=build_unknown(new_if.type(), write);
823  }
824  else if(op2_err)
825  {
826  new_if.type()=new_if.true_case().type();
827  new_if.false_case()=build_unknown(new_if.type(), write);
828  }
829  else
830  new_if.type()=new_if.true_case().type();
831 
832  dest.swap(new_if);
833  return false;
834 }
835 
837  exprt &dest, bool write)
838 {
839  assert(is_char_type(object.type().subtype()));
840 
841  // writing is invalid
842  if(write)
843  return true;
844 
845  const exprt &a_size=to_array_type(object.type()).size();
846  mp_integer size;
847  // don't do anything, if we cannot determine the size
848  if(to_integer(a_size, size))
849  return true;
850  assert(size==object.operands().size());
851 
852  exprt::operandst::const_iterator it=object.operands().begin();
853  for(mp_integer i=0; i<size; ++i, ++it)
854  if(it->is_zero())
855  return build_symbol_constant(i, size, dest);
856 
857  return true;
858 }
859 
861  exprt &dest, bool write)
862 {
863  assert(object.type().id()==ID_pointer);
864 
865  pointer_arithmetict ptr(object);
866  if(ptr.pointer.id()==ID_address_of)
867  {
869 
870  if(a.object().id()==ID_index)
871  return build_wrap(to_index_expr(a.object()).array(), dest, write);
872 
873  // writing is invalid
874  if(write)
875  return true;
876 
877  if(build_wrap(a.object(), dest, write))
878  return true;
879  dest=address_of_exprt(dest);
880  return false;
881  }
882  else if(ptr.pointer.id()==ID_symbol &&
883  is_char_type(object.type().subtype()))
884  // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
885  // checks
886  return build_wrap(ptr.pointer, dest, write);
887 
888  // we don't handle other pointer arithmetic
889  return true;
890 }
891 
893 {
894  typet type=build_type(what);
895 
896  if(write)
897  return exprt(ID_null_object, type);
898 
899  exprt result;
900 
901  switch(what)
902  {
903  case whatt::IS_ZERO:
905  break;
906 
907  case whatt::LENGTH:
908  case whatt::SIZE:
910  break;
911  }
912 
913  return result;
914 }
915 
917 {
918  if(write)
919  return exprt(ID_null_object, type);
920 
921  // create an uninitialized dummy symbol
922  // because of a lack of contextual information we can't build a nice name
923  // here, but moving that into locals should suffice for proper operation
924  irep_idt identifier=
925  "$tmp::nondet_str#str$"+std::to_string(++temporary_counter);
926  // ensure decl and initialization
927  locals[identifier]=identifier;
928 
929  auxiliary_symbolt new_symbol;
930  new_symbol.type=type;
931  new_symbol.value.make_nil();
932  new_symbol.name=identifier;
933  new_symbol.module="$tmp";
934  new_symbol.base_name=identifier;
935  new_symbol.mode=ID_C;
936  new_symbol.pretty_name=identifier;
937 
938  symbol_table.insert(std::move(new_symbol));
939 
940  return ns.lookup(identifier).symbol_expr();
941 }
942 
944 {
945  const symbolt &symbol=ns.lookup(sym.get_identifier());
946 
947  const typet &abstract_type=build_abstraction_type(symbol.type);
948  assert(!abstract_type.is_nil());
949 
950  irep_idt identifier="";
951 
952  if(current_args.find(symbol.name)!=current_args.end())
953  identifier=id2string(symbol.name)+arg_suffix;
954  else
955  {
956  identifier=id2string(symbol.name)+sym_suffix;
957  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
958  build_new_symbol(symbol, identifier, abstract_type);
959  }
960 
961  const symbolt &str_symbol=ns.lookup(identifier);
962  dest=str_symbol.symbol_expr();
963  if(current_args.find(symbol.name)!=current_args.end() &&
964  !is_ptr_argument(abstract_type))
965  dest=dereference_exprt(dest, dest.type().subtype());
966 
967  return false;
968 }
969 
971  const irep_idt &identifier, const typet &type)
972 {
973  if(!symbol.is_static_lifetime)
974  locals[symbol.name]=identifier;
975 
976  auxiliary_symbolt new_symbol;
977  new_symbol.type=type;
978  new_symbol.value.make_nil();
979  new_symbol.location=symbol.location;
980  new_symbol.name=identifier;
981  new_symbol.module=symbol.module;
982  new_symbol.base_name=id2string(symbol.base_name)+sym_suffix;
983  new_symbol.mode=symbol.mode;
984  new_symbol.pretty_name=
985  id2string(symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+
986  sym_suffix;
987  new_symbol.is_static_lifetime=symbol.is_static_lifetime;
988  new_symbol.is_thread_local=symbol.is_thread_local;
989 
990  symbol_table.insert(std::move(new_symbol));
991 
992  if(symbol.is_static_lifetime)
993  {
995  dummy_loc->source_location=symbol.location;
996  make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
997  initialization.instructions.erase(dummy_loc);
998  }
999 }
1000 
1002  const mp_integer &zero_length,
1003  const mp_integer &buf_size,
1004  exprt &dest)
1005 {
1006  irep_idt base="$string_constant_str_"+integer2string(zero_length)
1007  +"_"+integer2string(buf_size);
1008  irep_idt identifier="string_abstraction::"+id2string(base);
1009 
1010  if(symbol_table.symbols.find(identifier)==
1011  symbol_table.symbols.end())
1012  {
1013  auxiliary_symbolt new_symbol;
1014  new_symbol.type=string_struct;
1015  new_symbol.value.make_nil();
1016  new_symbol.name=identifier;
1017  new_symbol.base_name=base;
1018  new_symbol.mode=ID_C;
1019  new_symbol.pretty_name=base;
1020  new_symbol.is_static_lifetime=true;
1021  new_symbol.is_thread_local=false;
1022  new_symbol.is_file_local=false;
1023 
1024  {
1025  struct_exprt value(string_struct);
1026  value.operands().resize(3);
1027 
1028  value.op0()=true_exprt();
1029  value.op1()=from_integer(zero_length, build_type(whatt::LENGTH));
1030  value.op2()=from_integer(buf_size, build_type(whatt::SIZE));
1031 
1032  // initialization
1034  assignment1->make_assignment();
1035  assignment1->code=code_assignt(new_symbol.symbol_expr(), value);
1036  }
1037 
1038  symbol_table.insert(std::move(new_symbol));
1039  }
1040 
1041  dest=address_of_exprt(symbol_exprt(identifier, string_struct));
1042 
1043  return false;
1044 }
1045 
1047 {
1048  if(lhs.id()==ID_minus)
1049  {
1050  // move op1 to rhs
1051  exprt rest=lhs.op0();
1052  rhs=plus_exprt(rhs, lhs.op1());
1053  rhs.type()=lhs.type();
1054  lhs=rest;
1055  }
1056 }
1057 
1059  goto_programt &dest,
1060  goto_programt::targett target)
1061 {
1062  code_assignt &assign=to_code_assign(target->code);
1063 
1064  exprt &lhs=assign.lhs();
1065  exprt rhs=assign.rhs();
1066  exprt *rhsp=&(assign.rhs());
1067 
1068  while(rhsp->id()==ID_typecast)
1069  rhsp=&(rhsp->op0());
1070 
1071  const typet &abstract_type=build_abstraction_type(lhs.type());
1072  if(abstract_type.is_nil())
1073  return target;
1074 
1075  exprt new_lhs, new_rhs;
1076  if(build_wrap(lhs, new_lhs, true))
1077  return target;
1078 
1079  bool unknown=(abstract_type!=build_abstraction_type(rhsp->type()) ||
1080  build_wrap(rhs, new_rhs, false));
1081  if(unknown)
1082  new_rhs=build_unknown(abstract_type, false);
1083 
1084  if(lhs.type().id()==ID_pointer && !unknown)
1085  {
1086  goto_programt::instructiont assignment;
1087  assignment.make_assignment();
1088  assignment.source_location=target->source_location;
1089  assignment.function=target->function;
1090  assignment.code=code_assignt(new_lhs, new_rhs);
1091  assignment.code.add_source_location()=target->source_location;
1092  dest.insert_before_swap(target, assignment);
1093  ++target;
1094 
1095  return target;
1096  }
1097  else
1098  {
1099  return value_assignments(dest, target, new_lhs, new_rhs);
1100  }
1101 }
1102 
1104  goto_programt &dest,
1105  goto_programt::targett target)
1106 {
1107  code_assignt &assign=to_code_assign(target->code);
1108 
1109  exprt &lhs=assign.lhs();
1110  exprt *rhsp=&(assign.rhs());
1111 
1112  while(rhsp->id()==ID_typecast)
1113  rhsp=&(rhsp->op0());
1114 
1115  // we only care if the constant zero is assigned
1116  if(!rhsp->is_zero())
1117  return target;
1118 
1119  // index into a character array
1120  if(lhs.id()==ID_index)
1121  {
1122  const index_exprt &i_lhs=to_index_expr(lhs);
1123 
1124  exprt new_lhs;
1125  if(!build_wrap(i_lhs.array(), new_lhs, true))
1126  {
1127  exprt i2=member(new_lhs, whatt::LENGTH);
1128  assert(i2.is_not_nil());
1129 
1130  exprt new_length=i_lhs.index();
1131  make_type(new_length, i2.type());
1132 
1133  if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
1134  new_length, i2);
1135 
1136  return char_assign(dest, target, new_lhs, i2, min_expr);
1137  }
1138  }
1139  else if(lhs.id()==ID_dereference)
1140  {
1141  pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
1142  exprt new_lhs;
1143  if(!build_wrap(ptr.pointer, new_lhs, true))
1144  {
1145  const exprt i2=member(new_lhs, whatt::LENGTH);
1146  assert(i2.is_not_nil());
1147 
1149  return
1150  char_assign(
1151  dest,
1152  target,
1153  new_lhs,
1154  i2,
1155  ptr.offset.is_nil()?
1157  ptr.offset);
1158  }
1159  }
1160 
1161  return target;
1162 }
1163 
1165  goto_programt &dest,
1166  goto_programt::targett target,
1167  const exprt &new_lhs,
1168  const exprt &lhs,
1169  const exprt &rhs)
1170 {
1171  goto_programt tmp;
1172 
1173  const exprt i1=member(new_lhs, whatt::IS_ZERO);
1174  assert(i1.is_not_nil());
1175 
1176  goto_programt::targett assignment1=tmp.add_instruction();
1177  assignment1->make_assignment();
1178  assignment1->source_location=target->source_location;
1179  assignment1->function=target->function;
1180  assignment1->code=code_assignt(i1, true_exprt());
1181  assignment1->code.add_source_location()=target->source_location;
1182 
1183  goto_programt::targett assignment2=tmp.add_instruction();
1184  assignment2->make_assignment();
1185  assignment2->source_location=target->source_location;
1186  assignment2->function=target->function;
1187  assignment2->code=code_assignt(lhs, rhs);
1188  assignment2->code.add_source_location()=target->source_location;
1189 
1191  assignment2->code.op0(),
1192  assignment2->code.op1());
1193 
1194  dest.insert_before_swap(target, tmp);
1195  ++target;
1196  ++target;
1197 
1198  return target;
1199 }
1200 
1202  goto_programt &dest,
1203  goto_programt::targett target,
1204  const exprt &lhs,
1205  const exprt &rhs)
1206 {
1207  if(rhs.id()==ID_if)
1208  return value_assignments_if(dest, target, lhs, to_if_expr(rhs));
1209 
1210  assert(type_eq(lhs.type(), rhs.type(), ns));
1211 
1212  if(lhs.type().id()==ID_array)
1213  {
1214  const exprt &a_size=to_array_type(lhs.type()).size();
1215  mp_integer size;
1216  // don't do anything, if we cannot determine the size
1217  if(to_integer(a_size, size))
1218  return target;
1219  for(mp_integer i=0; i<size; ++i)
1220  target=value_assignments(dest, target,
1221  index_exprt(lhs, from_integer(i, a_size.type())),
1222  index_exprt(rhs, from_integer(i, a_size.type())));
1223  }
1224  else if(lhs.type().id()==ID_pointer)
1225  return value_assignments(dest, target,
1226  dereference_exprt(lhs, lhs.type().subtype()),
1227  dereference_exprt(rhs, rhs.type().subtype()));
1228  else if(lhs.type()==string_struct)
1229  return value_assignments_string_struct(dest, target, lhs, rhs);
1230  else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)
1231  {
1232  const struct_union_typet &struct_union_type=
1233  to_struct_union_type(lhs.type());
1234 
1235  for(const auto &comp : struct_union_type.components())
1236  {
1237  assert(!comp.get_name().empty());
1238 
1239  target=value_assignments(dest, target,
1240  member_exprt(lhs, comp.get_name(), comp.type()),
1241  member_exprt(rhs, comp.get_name(), comp.type()));
1242  }
1243  }
1244 
1245  return target;
1246 }
1247 
1249  goto_programt &dest,
1250  goto_programt::targett target,
1251  const exprt &lhs, const if_exprt &rhs)
1252 {
1253  goto_programt tmp;
1254 
1257  goto_programt::targett else_target=tmp.add_instruction(SKIP);
1259 
1260  goto_else->function=target->function;
1261  goto_else->source_location=target->source_location;
1262  goto_else->make_goto(else_target, rhs.cond());
1263  goto_else->guard.make_not();
1264 
1265  goto_out->function=target->function;
1266  goto_out->source_location=target->source_location;
1267  goto_out->make_goto(out_target, true_exprt());
1268 
1269  else_target->function=target->function;
1270  else_target->source_location=target->source_location;
1271 
1272  out_target->function=target->function;
1273  out_target->source_location=target->source_location;
1274 
1275  value_assignments(tmp, goto_out, lhs, rhs.true_case());
1276  value_assignments(tmp, else_target, lhs, rhs.false_case());
1277 
1278  goto_programt::targett last=target;
1279  ++last;
1280  dest.insert_before_swap(target, tmp);
1281  --last;
1282 
1283  return last;
1284 }
1285 
1287  goto_programt &dest,
1288  goto_programt::targett target,
1289  const exprt &lhs, const exprt &rhs)
1290 {
1291  // copy all the values
1292  goto_programt tmp;
1293 
1294  {
1296  assignment->code=code_assignt(
1297  member(lhs, whatt::IS_ZERO),
1298  member(rhs, whatt::IS_ZERO));
1299  assignment->code.add_source_location()=target->source_location;
1300  assignment->function=target->function;
1301  assignment->source_location=target->source_location;
1302  }
1303 
1304  {
1306  assignment->code=code_assignt(
1307  member(lhs, whatt::LENGTH),
1308  member(rhs, whatt::LENGTH));
1309  assignment->code.add_source_location()=target->source_location;
1310  assignment->function=target->function;
1311  assignment->source_location=target->source_location;
1312  }
1313 
1314  {
1316  assignment->code=code_assignt(
1317  member(lhs, whatt::SIZE),
1318  member(rhs, whatt::SIZE));
1319  assignment->code.add_source_location()=target->source_location;
1320  assignment->function=target->function;
1321  assignment->source_location=target->source_location;
1322  }
1323 
1324  goto_programt::targett last=target;
1325  ++last;
1326  dest.insert_before_swap(target, tmp);
1327  --last;
1328 
1329  return last;
1330 }
1331 
1333 {
1334  if(a.is_nil())
1335  return a;
1336 
1337  assert(type_eq(a.type(), string_struct, ns) ||
1338  is_ptr_string_struct(a.type()));
1339 
1340  exprt struct_op=
1341  a.type().id()==ID_pointer?
1343 
1344  irep_idt component_name;
1345 
1346  switch(what)
1347  {
1348  case whatt::IS_ZERO: component_name="is_zero"; break;
1349  case whatt::SIZE: component_name="size"; break;
1350  case whatt::LENGTH: component_name="length"; break;
1351  }
1352 
1353  member_exprt result(struct_op, component_name, build_type(what));
1354 
1355  return result;
1356 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
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:291
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
exprt & true_case()
Definition: std_expr.h:3393
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:172
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:44
bool is_not_nil() const
Definition: irep.h:173
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:3178
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
void make_type(exprt &dest, const typet &type)
void abstract_function_call(goto_programt::targett it)
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:993
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:3359
exprt & cond()
Definition: std_expr.h:3383
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:888
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:3199
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:3326
Extract member of struct or union.
Definition: std_expr.h:3869
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:240
const irep_idt & id() const
Definition: irep.h:259
::std::set< irep_idt > current_args
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
exprt & lhs()
Definition: std_code.h:209
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:4486
argumentst & arguments()
Definition: std_code.h:890
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:254
::std::map< typet, typet > abstraction_types_mapt
String Abstraction.
The NIL expression.
Definition: std_expr.h:4508
exprt & rhs()
Definition: std_code.h:214
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
Operator to dereference a pointer.
Definition: std_expr.h:3282
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:3953
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
int main()
const exprt & size() const
Definition: std_types.h:1023
A function call.
Definition: std_code.h:858
#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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:3168
exprt & false_case()
Definition: std_expr.h:3403
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:4497
const typet & build_abstraction_type(const typet &type)
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:878
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:1054
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
const exprt & struct_op() const
Definition: std_expr.h:3909
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:3893
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:271
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:315
void swap(irept &irep)
Definition: irep.h:303
#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:1013
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:32
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:73
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:136
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
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:909
array index operator
Definition: std_expr.h:1462