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