cprover
recursive_initialization.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: recursive_initialization
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
11 #include <util/allocate_objects.h>
12 #include <util/arith_tools.h>
13 #include <util/c_types.h>
14 #include <util/fresh_symbol.h>
15 #include <util/irep.h>
16 #include <util/optional_utils.h>
18 #include <util/rename.h>
19 #include <util/std_code.h>
20 #include <util/std_expr.h>
21 #include <util/string2int.h>
22 #include <util/string_utils.h>
23 
24 #include <functional>
25 #include <iterator>
26 
28  const std::string &option,
29  const std::list<std::string> &values)
30 {
32  {
33  auto const value =
35  auto const user_min_null_tree_depth =
36  string2optional<std::size_t>(value, 10);
37  if(user_min_null_tree_depth.has_value())
38  {
39  min_null_tree_depth = user_min_null_tree_depth.value();
40  }
41  else
42  {
44  "failed to convert '" + value + "' to integer",
46  }
47  return true;
48  }
50  {
51  auto const value =
53  auto const user_max_nondet_tree_depth =
54  string2optional<std::size_t>(value, 10);
55  if(user_max_nondet_tree_depth.has_value())
56  {
57  max_nondet_tree_depth = user_max_nondet_tree_depth.value();
58  }
59  else
60  {
62  "failed to convert '" + value + "' to integer",
64  }
65  return true;
66  }
68  {
71  return true;
72  }
74  {
77  return true;
78  }
80  {
81  std::transform(
82  values.begin(),
83  values.end(),
84  std::inserter(
87  [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
88  return true;
89  }
91  {
92  const auto list_of_members_string =
95  const auto list_of_members = split_string(list_of_members_string, ',');
96  for(const auto &member : list_of_members)
97  {
98  const auto selection_spec_strings = split_string(member, '.');
99 
100  selection_specs.push_back({});
101  auto &selection_spec = selection_specs.back();
102  std::transform(
103  selection_spec_strings.begin(),
104  selection_spec_strings.end(),
105  std::back_inserter(selection_spec),
106  [](const std::string &member_name_string) {
107  return irep_idt{member_name_string};
108  });
109  }
110  return true;
111  }
112  return false;
113 }
114 
116  recursive_initialization_configt initialization_config,
117  goto_modelt &goto_model)
118  : initialization_config(std::move(initialization_config)),
119  goto_model(goto_model),
120  max_depth_var_name(get_fresh_global_name(
121  "max_depth",
122  from_integer(
123  initialization_config.max_nondet_tree_depth,
124  signed_int_type()))),
125  min_depth_var_name(get_fresh_global_name(
126  "min_depth",
127  from_integer(
128  initialization_config.min_null_tree_depth,
129  signed_int_type())))
130 {
132  this->initialization_config.pointers_to_treat_equal.size());
133 }
134 
136  const exprt &lhs,
137  const exprt &depth,
138  code_blockt &body)
139 {
140  if(lhs.id() == ID_symbol && !initialization_config.selection_specs.empty())
141  {
142  auto lhs_id = to_symbol_expr(lhs).get_identifier();
143  for(const auto &selection_spec : initialization_config.selection_specs)
144  {
145  if(selection_spec.front() == lhs_id)
146  {
147  initialize_selected_member(lhs, depth, body, selection_spec);
148  return;
149  }
150  }
151  }
152  // special handling for the case that pointer arguments should be treated
153  // equal: if the equality is enforced (rather than the pointers may be equal),
154  // then we don't even build the constructor functions
155  if(lhs.id() == ID_symbol)
156  {
157  const auto maybe_cluster_index =
158  find_equal_cluster(to_symbol_expr(lhs).get_identifier());
159  if(maybe_cluster_index.has_value())
160  {
161  if(common_arguments_origins[*maybe_cluster_index].has_value())
162  {
163  const auto set_equal_case =
164  code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]};
166  {
167  const irep_idt &fun_name = build_constructor(lhs);
168  const symbolt &fun_symbol =
170  const auto proper_init_case = code_function_callt{
171  fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}}};
172 
173  body.add(code_ifthenelset{
175  set_equal_case,
176  proper_init_case});
177  }
178  else
179  {
180  body.add(set_equal_case);
181  }
182  return;
183  }
184  else
185  {
186  common_arguments_origins[*maybe_cluster_index] = lhs;
187  }
188  }
189  }
190 
191  const irep_idt &fun_name = build_constructor(lhs);
192  const symbolt &fun_symbol = goto_model.symbol_table.lookup_ref(fun_name);
193 
194  if(lhs.id() == ID_symbol)
195  {
196  const irep_idt &lhs_name = to_symbol_expr(lhs).get_identifier();
197  if(should_be_treated_as_array(lhs_name))
198  {
199  auto size_var = get_associated_size_variable(lhs_name);
200  if(size_var.has_value())
201  {
202  const symbol_exprt &size_symbol =
203  goto_model.symbol_table.lookup_ref(size_var.value()).symbol_expr();
205  fun_symbol.symbol_expr(),
206  {depth, address_of_exprt{lhs}, address_of_exprt{size_symbol}}});
207  }
208  else
209  {
210  const auto &fun_type_params =
211  to_code_type(fun_symbol.type).parameters();
212  const typet &size_var_type = fun_type_params.back().type();
214  fun_symbol.symbol_expr(),
215  {depth,
216  address_of_exprt{lhs},
217  null_pointer_exprt{pointer_type(size_var_type)}}});
218  }
219  return;
220  }
221  for(const auto &irep_pair :
223  {
224  // skip initialisation of array-size variables
225  if(irep_pair.second == lhs_name)
226  return;
227  }
228  }
229  body.add(code_function_callt{fun_symbol.symbol_expr(),
230  {depth, address_of_exprt{lhs}}});
231 }
232 
234  const exprt &depth_symbol,
236  const optionalt<exprt> &size_symbol,
237  const optionalt<irep_idt> &lhs_name,
238  const bool is_nullable)
239 {
240  PRECONDITION(result_symbol.type().id() == ID_pointer);
241  const typet &type = result_symbol.type().subtype();
242  if(type.id() == ID_struct_tag)
243  {
244  return build_struct_constructor(depth_symbol, result_symbol);
245  }
246  else if(type.id() == ID_pointer)
247  {
248  if(type.subtype().id() == ID_code)
249  {
251  }
252  if(lhs_name.has_value())
253  {
254  if(should_be_treated_as_cstring(*lhs_name) && type == char_type())
256  else if(should_be_treated_as_array(*lhs_name))
257  {
258  CHECK_RETURN(size_symbol.has_value());
260  depth_symbol, result_symbol, *size_symbol, lhs_name);
261  }
262  }
263  return build_pointer_constructor(depth_symbol, result_symbol);
264  }
265  else if(type.id() == ID_array)
266  {
267  return build_array_constructor(depth_symbol, result_symbol);
268  }
269  else
270  {
272  }
273 }
274 
276 {
277  // for `expr` of type T builds a declaration of a function:
278  //
279  // void type_constructor_T(int depth_T, T *result);
280  //
281  // or in case a `size` is associated with the `expr`
282  //
283  // void type_constructor_T(int depth_T, T *result_T, int *size);
284  optionalt<irep_idt> size_var;
285  optionalt<irep_idt> expr_name;
286  bool is_nullable = false;
287  bool has_size_param = false;
288  if(expr.id() == ID_symbol)
289  {
290  expr_name = to_symbol_expr(expr).get_identifier();
292  expr_name.value());
293  if(should_be_treated_as_array(*expr_name))
294  {
295  size_var = get_associated_size_variable(*expr_name);
296  has_size_param = true;
297  }
298  }
299  const typet &type = expr.type();
300  const constructor_keyt key{type, is_nullable, has_size_param};
301  if(type_constructor_names.find(key) != type_constructor_names.end())
302  return type_constructor_names[key];
303 
304  const std::string &pretty_type = type2id(type);
305  symbolt &depth_symbol =
306  get_fresh_param_symbol("depth_" + pretty_type, signed_int_type());
307  depth_symbol.value = from_integer(0, signed_int_type());
308 
309  code_typet::parameterst fun_params;
310  code_typet::parametert depth_parameter{signed_int_type()};
311  depth_parameter.set_identifier(depth_symbol.name);
312  fun_params.push_back(depth_parameter);
313 
314  const typet &result_type = pointer_type(type);
315  const symbolt &result_symbol =
316  get_fresh_param_symbol("result_" + pretty_type, result_type);
317  code_typet::parametert result_parameter{result_type};
318  result_parameter.set_identifier(result_symbol.name);
319  fun_params.push_back(result_parameter);
320 
321  auto &symbol_table = goto_model.symbol_table;
322  optionalt<exprt> size_symbol_expr;
323  if(expr_name.has_value() && should_be_treated_as_array(*expr_name))
324  {
325  typet size_var_type;
326  if(size_var.has_value())
327  {
328  const symbol_exprt &size_var_symbol_expr =
329  symbol_table.lookup_ref(*size_var).symbol_expr();
330  size_var_type = pointer_type(size_var_symbol_expr.type());
331  }
332  else
333  size_var_type = pointer_type(signed_int_type());
334 
335  const symbolt &size_symbol =
336  get_fresh_param_symbol("size_" + pretty_type, size_var_type);
337  fun_params.push_back(code_typet::parametert{size_var_type});
338  fun_params.back().set_identifier(size_symbol.name);
339  size_symbol_expr = size_symbol.symbol_expr();
340  }
341  const symbolt &function_symbol = get_fresh_fun_symbol(
342  "type_constructor_" + pretty_type, code_typet{fun_params, empty_typet{}});
343  type_constructor_names[key] = function_symbol.name;
344  symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.name);
345 
346  // the body is specific for each type of expression
347  mutable_symbol->value = build_constructor_body(
348  depth_symbol.symbol_expr(),
350  size_symbol_expr,
351  // the expression name may be needed to decide if expr should be treated as
352  // a string
353  expr_name,
354  is_nullable);
355 
356  goto_model.goto_functions.function_map[function_symbol.name].type =
357  to_code_type(function_symbol.type);
358  return type_constructor_names.at(key);
359 }
360 
362 {
363  auto malloc_sym = goto_model.symbol_table.lookup("malloc");
364  if(malloc_sym == nullptr)
365  {
366  symbolt new_malloc_sym;
367  new_malloc_sym.type = code_typet{code_typet{
369  new_malloc_sym.name = new_malloc_sym.pretty_name =
370  new_malloc_sym.base_name = "malloc";
371  new_malloc_sym.mode = initialization_config.mode;
372  goto_model.symbol_table.insert(new_malloc_sym);
373  return new_malloc_sym.symbol_expr();
374  }
375  return malloc_sym->symbol_expr();
376 }
377 
379  const irep_idt &array_name) const
380 {
383 }
384 
387 {
388  for(equal_cluster_idt index = 0;
390  ++index)
391  {
392  if(initialization_config.pointers_to_treat_equal[index].count(name) != 0)
393  return index;
394  }
395  return {};
396 }
397 
399  const irep_idt &cmdline_arg) const
400 {
402  cmdline_arg) !=
404 }
405 
407  const irep_idt &array_name) const
408 {
409  return optional_lookup(
411  array_name);
412 }
413 
415  const irep_idt &pointer_name) const
416 {
418  pointer_name) != 0;
419 }
420 
422 {
423  std::ostringstream out{};
424  out << "recursive_initialization_config {"
425  << "\n min_null_tree_depth = " << min_null_tree_depth
426  << "\n max_nondet_tree_depth = " << max_nondet_tree_depth
427  << "\n mode = " << mode
428  << "\n max_dynamic_array_size = " << max_dynamic_array_size
429  << "\n min_dynamic_array_size = " << min_dynamic_array_size
430  << "\n pointers_to_treat_as_arrays = [";
431  for(auto const &pointer : pointers_to_treat_as_arrays)
432  {
433  out << "\n " << pointer;
434  }
435  out << "\n ]"
436  << "\n variables_that_hold_array_sizes = [";
437  for(auto const &array_size : variables_that_hold_array_sizes)
438  {
439  out << "\n " << array_size;
440  }
441  out << "\n ]";
442  out << "\n array_name_to_associated_size_variable = [";
443  for(auto const &associated_array_size :
445  {
446  out << "\n " << associated_array_size.first << " -> "
447  << associated_array_size.second;
448  }
449  out << "\n ]";
450  out << "\n pointers_to_treat_as_cstrings = [";
451  for(const auto &pointer_to_treat_as_string_name :
453  {
454  out << "\n " << pointer_to_treat_as_string_name << std::endl;
455  }
456  out << "\n ]";
457  out << "\n}";
458  return out.str();
459 }
460 
462  const std::string &symbol_name,
463  const exprt &initial_value) const
464 {
465  symbolt &fresh_symbol = get_fresh_aux_symbol(
466  signed_int_type(),
468  symbol_name,
472  fresh_symbol.is_static_lifetime = true;
473  fresh_symbol.is_lvalue = true;
474  fresh_symbol.value = initial_value;
475  return fresh_symbol.name;
476 }
477 
479  const std::string &symbol_name) const
480 {
481  symbolt &fresh_symbol = get_fresh_aux_symbol(
482  signed_int_type(),
484  symbol_name,
488  fresh_symbol.is_static_lifetime = true;
489  fresh_symbol.is_lvalue = true;
490  fresh_symbol.value = from_integer(0, signed_int_type());
491  return fresh_symbol.symbol_expr();
492 }
493 
495  const std::string &symbol_name) const
496 {
497  symbolt &fresh_symbol = get_fresh_aux_symbol(
498  signed_int_type(),
500  symbol_name,
504  fresh_symbol.is_lvalue = true;
505  fresh_symbol.value = from_integer(0, signed_int_type());
506  return fresh_symbol.symbol_expr();
507 }
508 
510  const std::string &symbol_name,
511  const typet &type,
512  const exprt &init_value) const
513 {
514  symbolt &fresh_symbol = get_fresh_aux_symbol(
515  type,
517  symbol_name,
521  fresh_symbol.is_lvalue = true;
522  fresh_symbol.value = init_value;
523  return fresh_symbol.symbol_expr();
524 }
525 
527  const std::string &fun_name,
528  const typet &fun_type)
529 {
530  irep_idt fresh_name(fun_name);
531 
532  get_new_name(fresh_name, namespacet{goto_model.symbol_table}, '_');
533 
534  // create the function symbol
535  symbolt function_symbol{};
536  function_symbol.name = function_symbol.base_name =
537  function_symbol.pretty_name = fresh_name;
538 
539  function_symbol.is_lvalue = true;
540  function_symbol.mode = initialization_config.mode;
541  function_symbol.type = fun_type;
542 
543  auto r = goto_model.symbol_table.insert(function_symbol);
544  CHECK_RETURN(r.second);
545  return *goto_model.symbol_table.lookup(fresh_name);
546 }
547 
549  const std::string &symbol_name,
550  const typet &symbol_type)
551 {
552  symbolt &param_symbol = get_fresh_aux_symbol(
553  symbol_type,
555  symbol_name,
559  param_symbol.is_parameter = true;
560  param_symbol.is_lvalue = true;
561 
562  return param_symbol;
563 }
564 
567 {
568  auto maybe_symbol = goto_model.symbol_table.lookup(symbol_name);
569  CHECK_RETURN(maybe_symbol != nullptr);
570  return maybe_symbol->symbol_expr();
571 }
572 
573 std::string recursive_initializationt::type2id(const typet &type) const
574 {
575  if(type.id() == ID_struct_tag)
576  {
577  auto st_tag = id2string(to_struct_tag_type(type).get_identifier());
578  std::replace(st_tag.begin(), st_tag.end(), '-', '_');
579  return st_tag;
580  }
581  else if(type.id() == ID_pointer)
582  return "ptr_" + type2id(type.subtype());
583  else if(type.id() == ID_array)
584  {
585  const auto array_size =
586  numeric_cast_v<std::size_t>(to_constant_expr(to_array_type(type).size()));
587  return "arr_" + type2id(type.subtype()) + "_" + std::to_string(array_size);
588  }
589  else if(type == char_type())
590  return "char";
591  else if(type.id() == ID_signedbv)
592  return "int";
593  else if(type.id() == ID_unsignedbv)
594  return "uint";
595  else
596  return "";
597 }
598 
600 {
601  auto free_sym = goto_model.symbol_table.lookup("free");
602  if(free_sym == nullptr)
603  {
604  symbolt new_free_sym;
605  new_free_sym.type = code_typet{code_typet{
607  new_free_sym.name = new_free_sym.pretty_name = new_free_sym.base_name =
608  "free";
609  new_free_sym.mode = initialization_config.mode;
610  goto_model.symbol_table.insert(new_free_sym);
611  return new_free_sym.symbol_expr();
612  }
613  return free_sym->symbol_expr();
614 }
615 
617  const exprt &depth,
618  const symbol_exprt &result)
619 {
620  PRECONDITION(result.type().id() == ID_pointer);
621  const typet &type = result.type().subtype();
622  PRECONDITION(type.id() == ID_pointer);
623 
624  code_blockt body{};
625 
626  // build:
627  // void type_constructor_ptr_T(int depth, T** result)
628  // {
629  // if(has_seen && depth >= max_depth)
630  // *result=NULL;
631  // else if(depth < min_null_tree_depth || nondet()) {
632  // size_t has_seen_prev;
633  // has_seen_prev = T_has_seen;
634  // T_has_seen = 1;
635  // *result = malloc(sizeof(T));
636  // type_constructor_T(depth+1, *result);
637  // T_has_seen=has_seen_prev;
638  // }
639  // else
640  // *result=NULL;
641  // }
642 
643  binary_predicate_exprt depth_gt_max_depth{
644  depth, ID_ge, get_symbol_expr(max_depth_var_name)};
645  exprt::operandst should_not_recurse{depth_gt_max_depth};
646 
647  optionalt<symbol_exprt> has_seen;
649  has_seen = get_fresh_global_symexpr("has_seen_" + type2id(type.subtype()));
650 
651  if(has_seen.has_value())
652  {
653  equal_exprt has_seen_expr{*has_seen, from_integer(1, has_seen->type())};
654  should_not_recurse.push_back(has_seen_expr);
655  }
656 
657  null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
658  code_blockt null_and_return{};
659  code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
660  null_and_return.add(assign_null);
661  null_and_return.add(code_returnt{});
662  body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
663 
664  exprt::operandst should_recurse_ops{
667  code_blockt then_case{};
668 
669  code_assignt seen_assign_prev{};
670  if(has_seen.has_value())
671  {
672  const symbol_exprt &has_seen_prev =
673  get_fresh_local_symexpr("has_seen_prev_" + type2id(type.subtype()));
674  then_case.add(code_declt{has_seen_prev});
675  then_case.add(code_assignt{has_seen_prev, *has_seen});
676  then_case.add(code_assignt{*has_seen, from_integer(1, has_seen->type())});
677  seen_assign_prev = code_assignt{*has_seen, has_seen_prev};
678  }
679 
680  const symbol_exprt &local_result =
681  get_fresh_local_typed_symexpr("local_result", type, nullptr_expr);
682  then_case.add(code_declt{local_result});
684  then_case.add(code_function_callt{
685  local_result, get_malloc_function(), {*size_of_expr(type.subtype(), ns)}});
686  initialize(
687  dereference_exprt{local_result},
688  plus_exprt{depth, from_integer(1, depth.type())},
689  then_case);
690  then_case.add(code_assignt{dereference_exprt{result}, local_result});
691 
692  if(has_seen.has_value())
693  {
694  then_case.add(seen_assign_prev);
695  }
696 
697  body.add(
698  code_ifthenelset{disjunction(should_recurse_ops), then_case, assign_null});
699  return body;
700 }
701 
703  const symbol_exprt &result) const
704 {
705  PRECONDITION(result.type().id() == ID_pointer);
706  const typet &type = result.type().subtype();
707  PRECONDITION(type.id() == ID_array);
708  PRECONDITION(type.subtype() == char_type());
709  const array_typet &array_type = to_array_type(type);
710  const auto array_size =
711  numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
712  code_blockt body{};
713 
714  for(std::size_t index = 0; index < array_size - 1; index++)
715  {
716  index_exprt index_expr{dereference_exprt{result},
717  from_integer(index, size_type())};
718  body.add(code_assignt{
720  body.add(code_assumet{
721  notequal_exprt{index_expr, from_integer(0, array_type.subtype())}});
722  }
724  from_integer(array_size - 1, size_type())},
725  from_integer(0, array_type.subtype())});
726 
727  return body;
728 }
729 
731  const exprt &depth,
732  const symbol_exprt &result)
733 {
734  PRECONDITION(result.type().id() == ID_pointer);
735  const typet &type = result.type().subtype();
736  PRECONDITION(type.id() == ID_array);
737  const array_typet &array_type = to_array_type(type);
738  const auto array_size =
739  numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
740  code_blockt body{};
741 
742  for(std::size_t index = 0; index < array_size; index++)
743  {
744  initialize(
746  depth,
747  body);
748  }
749  return body;
750 }
751 
753  const exprt &depth,
754  const symbol_exprt &result)
755 {
756  PRECONDITION(result.type().id() == ID_pointer);
757  const typet &struct_type = result.type().subtype();
758  PRECONDITION(struct_type.id() == ID_struct_tag);
759  code_blockt body{};
761  for(const auto &component :
762  ns.follow_tag(to_struct_tag_type(struct_type)).components())
763  {
764  initialize(member_exprt{dereference_exprt{result}, component}, depth, body);
765  }
766  return body;
767 }
768 
770  const symbol_exprt &result) const
771 {
772  PRECONDITION(result.type().id() == ID_pointer);
773  code_blockt body{};
774  body.add(code_assignt{
775  dereference_exprt{result},
776  side_effect_expr_nondett{result.type().subtype(), source_locationt{}}});
777  return body;
778 }
779 
781  const exprt &depth,
782  const symbol_exprt &result,
783  const exprt &size,
784  const optionalt<irep_idt> &lhs_name)
785 {
786  PRECONDITION(result.type().id() == ID_pointer);
787  const typet &pointer_type = result.type().subtype();
788  PRECONDITION(pointer_type.id() == ID_pointer);
789  const typet &element_type = pointer_type.subtype();
790 
791  // builds:
792  // void type_constructor_ptr_T(int depth, T** result, int* size)
793  // {
794  // int nondet_size;
795  // assume(nondet_size >= min_array_size && nondet_size <= max_array_size);
796  // T* local_result = malloc(nondet_size * sizeof(T));
797  // for (int i = 0; i < nondet_size; ++i)
798  // {
799  // type_construct_T(depth+1, local_result+i);
800  // }
801  // *result = local_result;
802  // if (size!=NULL)
803  // *size = nondet_size;
804  // }
805 
806  const auto min_array_size = initialization_config.min_dynamic_array_size;
807  const auto max_array_size = initialization_config.max_dynamic_array_size;
808  PRECONDITION(max_array_size >= min_array_size);
809 
810  code_blockt body{};
811  const symbol_exprt &nondet_size = get_fresh_local_symexpr("nondet_size");
812  body.add(code_declt{nondet_size});
813 
814  body.add(code_assumet{and_exprt{
816  nondet_size, ID_ge, from_integer(min_array_size, nondet_size.type())},
818  nondet_size, ID_le, from_integer(max_array_size, nondet_size.type())}}});
819 
820  const symbol_exprt &local_result =
822  body.add(code_declt{local_result});
824  for(auto array_size = min_array_size; array_size <= max_array_size;
825  ++array_size)
826  {
827  body.add(code_ifthenelset{
828  equal_exprt{nondet_size, from_integer(array_size, nondet_size.type())},
829  code_function_callt{local_result,
831  {mult_exprt{from_integer(array_size, size_type()),
832  *size_of_expr(element_type, ns)}}}});
833  }
834 
835  const symbol_exprt &index_iter = get_fresh_local_symexpr("index");
836  body.add(code_declt{index_iter});
837  code_assignt for_init{index_iter, from_integer(0, index_iter.type())};
838  binary_relation_exprt for_cond{index_iter, ID_lt, nondet_size};
839  side_effect_exprt for_iter{
840  ID_preincrement, {index_iter}, typet{}, source_locationt{}};
841  code_blockt for_body{};
842  if(lhs_name.has_value() && should_be_treated_as_cstring(*lhs_name))
843  {
844  code_blockt else_case{};
845  initialize(
846  dereference_exprt{plus_exprt{local_result, index_iter}},
847  plus_exprt{depth, from_integer(1, depth.type())},
848  else_case);
849  else_case.add(code_assumet{
850  notequal_exprt{dereference_exprt{plus_exprt{local_result, index_iter}},
851  from_integer(0, char_type())}});
852 
853  for_body.add(code_ifthenelset{
854  equal_exprt{
855  index_iter,
856  minus_exprt{nondet_size, from_integer(1, nondet_size.type())}},
857  code_assignt{dereference_exprt{plus_exprt{local_result, index_iter}},
858  from_integer(0, char_type())},
859  else_case});
860  }
861  else
862  {
863  initialize(
864  dereference_exprt{plus_exprt{local_result, index_iter}},
865  plus_exprt{depth, from_integer(1, depth.type())},
866  for_body);
867  }
868 
869  body.add(code_fort{for_init, for_cond, for_iter, for_body});
870  body.add(code_assignt{dereference_exprt{result}, local_result});
871 
872  CHECK_RETURN(size.type().id() == ID_pointer);
873  body.add(code_ifthenelset{
875  code_assignt{
876  dereference_exprt{size},
877  typecast_exprt::conditional_cast(nondet_size, size.type().subtype())}});
878 
879  return body;
880 }
881 
883 {
884  if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code)
885  return false;
886  for(auto const &common_arguments_origin : common_arguments_origins)
887  {
888  if(common_arguments_origin.has_value() && expr.id() == ID_symbol)
889  {
890  auto origin_name =
891  to_symbol_expr(*common_arguments_origin).get_identifier();
892  auto expr_name = to_symbol_expr(expr).get_identifier();
893  return origin_name == expr_name;
894  }
895  }
896  return true;
897 }
898 
900  const exprt &expr,
901  code_blockt &body)
902 {
903  PRECONDITION(expr.id() == ID_symbol);
904  const auto expr_id = to_symbol_expr(expr).get_identifier();
905  const auto maybe_cluster_index = find_equal_cluster(expr_id);
906  const auto call_free = code_function_callt{get_free_function(), {expr}};
907  if(!maybe_cluster_index.has_value())
908  {
909  // not in any equality cluster -> just free
910  body.add(call_free);
911  return;
912  }
913 
914  if(
915  to_symbol_expr(*common_arguments_origins[*maybe_cluster_index])
916  .get_identifier() != expr_id &&
918  {
919  // in equality cluster but not common origin -> free if not equal to origin
920  const auto condition =
921  notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]};
922  body.add(code_ifthenelset{condition, call_free});
923  }
924  else
925  {
926  // expr is common origin, leave freeing until the rest of the cluster is
927  // freed
928  return;
929  }
930 }
931 
933 {
934  for(auto const &origin : common_arguments_origins)
935  {
936  body.add(code_function_callt{get_free_function(), {*origin}});
937  }
938 }
939 
941  const symbol_exprt &result,
942  bool is_nullable)
943 {
945  const auto &result_type = to_pointer_type(result.type());
946  PRECONDITION(can_cast_type<pointer_typet>(result_type.subtype()));
947  const auto &function_pointer_type = to_pointer_type(result_type.subtype());
948  PRECONDITION(can_cast_type<code_typet>(function_pointer_type.subtype()));
949  const auto &function_type = to_code_type(function_pointer_type.subtype());
950 
951  std::vector<exprt> targets;
952 
953  for(const auto &sym : goto_model.get_symbol_table())
954  {
955  if(sym.second.type == function_type)
956  {
957  targets.push_back(address_of_exprt{sym.second.symbol_expr()});
958  }
959  }
960 
961  if(is_nullable)
962  targets.push_back(null_pointer_exprt{function_pointer_type});
963 
964  code_blockt body{};
965 
966  const auto function_pointer_selector =
967  get_fresh_local_symexpr("function_pointer_selector");
968  body.add(
969  code_assignt{function_pointer_selector,
970  side_effect_expr_nondett{function_pointer_selector.type(),
971  source_locationt{}}});
972  auto function_pointer_index = std::size_t{0};
973 
974  for(const auto &target : targets)
975  {
976  auto const assign = code_assignt{dereference_exprt{result}, target};
977  if(function_pointer_index != targets.size() - 1)
978  {
979  auto const condition = equal_exprt{
980  function_pointer_selector,
981  from_integer(function_pointer_index, function_pointer_selector.type())};
982  auto const then = code_blockt{{assign, code_returnt{}}};
983  body.add(code_ifthenelset{condition, then});
984  }
985  else
986  {
987  body.add(assign);
988  }
989  ++function_pointer_index;
990  }
991 
992  return body;
993 }
994 
996  const exprt &lhs,
997  const exprt &depth,
998  code_blockt &body,
999  const std::vector<irep_idt> &selection_spec)
1000 {
1001  PRECONDITION(lhs.id() == ID_symbol);
1002  PRECONDITION(lhs.type().id() == ID_struct_tag);
1003  PRECONDITION(!selection_spec.empty());
1004 
1005  auto component_member = lhs;
1007 
1008  for(auto it = selection_spec.begin() + 1; it != selection_spec.end(); it++)
1009  {
1010  if(component_member.type().id() != ID_struct_tag)
1011  {
1013  "'" + id2string(*it) + "' is not a component name",
1015  }
1016  const auto &struct_tag_type = to_struct_tag_type(component_member.type());
1017  const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
1018 
1019  bool found = false;
1020  for(auto const &component : struct_type.components())
1021  {
1022  const auto &component_type = component.type();
1023  const auto component_name = component.get_name();
1024 
1025  if(*it == component_name)
1026  {
1027  component_member =
1028  member_exprt{component_member, component_name, component_type};
1029  found = true;
1030  break;
1031  }
1032  }
1033  if(!found)
1034  {
1036  "'" + id2string(*it) + "' is not a component name",
1038  }
1039  }
1040  initialize(component_member, depth, body);
1041 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
recursive_initialization_configt::pointers_to_treat_as_cstrings
std::set< irep_idt > pointers_to_treat_as_cstrings
Definition: recursive_initialization.h:40
array_name
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:20
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:173
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2050
COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
Definition: common_harness_generator_options.h:17
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
recursive_initializationt::min_depth_var_name
irep_idt min_depth_var_name
Definition: recursive_initialization.h:121
arith_tools.h
recursive_initializationt::build_array_constructor
code_blockt build_array_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for arrays: simply iterates over elements and initialise each one.
Definition: recursive_initialization.cpp:730
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
recursive_initializationt::get_fresh_local_typed_symexpr
symbol_exprt get_fresh_local_typed_symexpr(const std::string &symbol_name, const typet &type, const exprt &init_value) const
Construct a new local symbol of type type initialised to init_value.
Definition: recursive_initialization.cpp:509
recursive_initializationt::goto_model
goto_modelt & goto_model
Definition: recursive_initialization.h:119
get_new_name
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
Definition: rename.cpp:19
recursive_initializationt::get_symbol_expr
symbol_exprt get_symbol_expr(const irep_idt &symbol_name) const
Recover the symbol expression from symbol table.
Definition: recursive_initialization.cpp:566
code_fort
codet representation of a for statement.
Definition: std_code.h:1023
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
recursive_initialization.h
fresh_symbol.h
recursive_initializationt::build_constructor
irep_idt build_constructor(const exprt &expr)
Check if a constructor for the type of expr already exists and create it if not.
Definition: recursive_initialization.cpp:275
recursive_initializationt::initialize_selected_member
void initialize_selected_member(const exprt &lhs, const exprt &depth, code_blockt &body, const std::vector< irep_idt > &selection_spec)
Select the specified struct-member to be non-deterministically initialized.
Definition: recursive_initialization.cpp:995
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
recursive_initializationt::get_malloc_function
symbol_exprt get_malloc_function()
Get the malloc function as symbol exprt, and inserts it into the goto-model if it doesn't exist alrea...
Definition: recursive_initialization.cpp:361
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2917
recursive_initializationt::get_associated_size_variable
optionalt< irep_idt > get_associated_size_variable(const irep_idt &array_name) const
Definition: recursive_initialization.cpp:406
recursive_initializationt::get_fresh_local_symexpr
symbol_exprt get_fresh_local_symexpr(const std::string &symbol_name) const
Construct a new local symbol of type int initialised to 0.
Definition: recursive_initialization.cpp:494
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT
#define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT
Definition: common_harness_generator_options.h:19
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:405
and_exprt
Boolean AND.
Definition: std_expr.h:2166
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:887
recursive_initialization_configt::array_name_to_associated_array_size_variable
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
Definition: recursive_initialization.h:38
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
recursive_initialization_configt::selection_specs
std::vector< std::vector< irep_idt > > selection_specs
Definition: recursive_initialization.h:45
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
bool_typet
The Boolean type.
Definition: std_types.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
harness_options_parser::require_exactly_one_value
std::string require_exactly_one_value(const std::string &option, const std::list< std::string > &values)
Returns the only value of a single element list, throws an exception if not passed a single element l...
Definition: goto_harness_generator.cpp:21
recursive_initialization_configt::mode
irep_idt mode
Definition: recursive_initialization.h:29
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
equal_exprt
Equality.
Definition: std_expr.h:1196
recursive_initializationt::free_cluster_origins
void free_cluster_origins(code_blockt &body)
Definition: recursive_initialization.cpp:932
recursive_initializationt::is_array_size_parameter
bool is_array_size_parameter(const irep_idt &cmdline_arg) const
Definition: recursive_initialization.cpp:398
recursive_initializationt::initialize
void initialize(const exprt &lhs, const exprt &depth, code_blockt &body)
Generate initialisation code for lhs into body.
Definition: recursive_initialization.cpp:135
recursive_initializationt::find_equal_cluster
optionalt< equal_cluster_idt > find_equal_cluster(const irep_idt &name) const
Definition: recursive_initialization.cpp:386
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:749
notequal_exprt
Disequality.
Definition: std_expr.h:1254
recursive_initializationt::build_function_pointer_constructor
code_blockt build_function_pointer_constructor(const symbol_exprt &result, bool is_nullable)
Constructor for function pointers.
Definition: recursive_initialization.cpp:940
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
recursive_initializationt::constructor_keyt
Definition: recursive_initialization.h:67
recursive_initialization_configt::pointers_to_treat_as_arrays
std::set< irep_idt > pointers_to_treat_as_arrays
Definition: recursive_initialization.h:36
recursive_initializationt::should_be_treated_as_array
bool should_be_treated_as_array(const irep_idt &pointer_name) const
Definition: recursive_initialization.cpp:378
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
recursive_initializationt::needs_freeing
bool needs_freeing(const exprt &expr) const
Definition: recursive_initialization.cpp:882
recursive_initialization_configt::max_nondet_tree_depth
std::size_t max_nondet_tree_depth
Definition: recursive_initialization.h:28
recursive_initializationt::get_fresh_param_symbol
symbolt & get_fresh_param_symbol(const std::string &param_name, const typet &param_type)
Construct a new parameter symbol of type param_type.
Definition: recursive_initialization.cpp:548
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1186
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
Definition: string_utils.cpp:40
can_cast_type< code_typet >
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:933
recursive_initialization_configt::max_dynamic_array_size
std::size_t max_dynamic_array_size
Definition: recursive_initialization.h:33
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
result_symbol
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:597
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
rename.h
recursive_initializationt::build_pointer_constructor
code_blockt build_pointer_constructor(const exprt &depth, const symbol_exprt &result)
Generic constructor for all pointers: only builds one pointee (not an array) but may recourse in case...
Definition: recursive_initialization.cpp:616
recursive_initialization_configt::arguments_may_be_equal
bool arguments_may_be_equal
Definition: recursive_initialization.h:43
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4018
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
recursive_initialization_configt::potential_null_function_pointers
std::unordered_set< irep_idt > potential_null_function_pointers
Definition: recursive_initialization.h:30
can_cast_type< struct_tag_typet >
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
Definition: std_types.h:502
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
recursive_initializationt::get_fresh_global_symexpr
symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const
Construct a new global symbol of type int initialised to 0.
Definition: recursive_initialization.cpp:478
recursive_initializationt::type_constructor_names
type_constructor_namest type_constructor_names
Definition: recursive_initialization.h:122
optional_utils.h
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
optional_lookup
auto optional_lookup(const map_like_collectiont &map, const keyt &key) -> optionalt< decltype(map.find(key) ->second)>
Lookup a key in a map, if found return the associated value, nullopt otherwise.
Definition: optional_utils.h:17
recursive_initializationt::build_array_string_constructor
code_blockt build_array_string_constructor(const symbol_exprt &result) const
Constructor for strings: as array but the last element is zero.
Definition: recursive_initialization.cpp:702
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:538
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
recursive_initializationt::build_dynamic_array_constructor
code_blockt build_dynamic_array_constructor(const exprt &depth, const symbol_exprt &result, const exprt &size, const optionalt< irep_idt > &lhs_name)
Constructor for dynamic arrays: allocate memory for n elements (n is random but bounded) and initiali...
Definition: recursive_initialization.cpp:780
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:992
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
irept::id
const irep_idt & id() const
Definition: irep.h:418
COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT
#define COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT
Definition: common_harness_generator_options.h:13
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_blockt::add
void add(const codet &code)
Definition: std_code.h:211
recursive_initializationt::recursive_initializationt
recursive_initializationt(recursive_initialization_configt initialization_config, goto_modelt &goto_model)
Definition: recursive_initialization.cpp:115
recursive_initializationt::get_fresh_fun_symbol
const symbolt & get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type)
Construct a new function symbol of type fun_type.
Definition: recursive_initialization.cpp:526
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
recursive_initializationt::get_fresh_global_name
irep_idt get_fresh_global_name(const std::string &symbol_name, const exprt &initial_value) const
Construct a new global symbol of type int and set it's value to initial_value.
Definition: recursive_initialization.cpp:461
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
recursive_initializationt::common_arguments_origins
std::vector< optionalt< exprt > > common_arguments_origins
Definition: recursive_initialization.h:123
recursive_initialization_configt::handle_option
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
Definition: recursive_initialization.cpp:27
minus_exprt
Binary minus.
Definition: std_expr.h:946
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
source_locationt
Definition: source_location.h:20
recursive_initializationt::build_constructor_body
code_blockt build_constructor_body(const exprt &depth_symbol, const symbol_exprt &result_symbol, const optionalt< exprt > &size_symbol, const optionalt< irep_idt > &lhs_name, const bool is_nullable)
Case analysis for which constructor should be used.
Definition: recursive_initialization.cpp:233
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1955
recursive_initializationt::free_if_possible
void free_if_possible(const exprt &expr, code_blockt &body)
Definition: recursive_initialization.cpp:899
recursive_initialization_configt::variables_that_hold_array_sizes
std::set< irep_idt > variables_that_hold_array_sizes
Definition: recursive_initialization.h:37
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1513
recursive_initializationt::should_be_treated_as_cstring
bool should_be_treated_as_cstring(const irep_idt &pointer_name) const
Definition: recursive_initialization.cpp:414
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3434
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
array_typet
Arrays with given size.
Definition: std_types.h:965
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1313
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
recursive_initializationt::type2id
std::string type2id(const typet &type) const
Simple pretty-printer for typet.
Definition: recursive_initialization.cpp:573
COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
Definition: common_harness_generator_options.h:15
recursive_initialization_configt::min_dynamic_array_size
std::size_t min_dynamic_array_size
Definition: recursive_initialization.h:34
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
recursive_initializationt::get_free_function
symbol_exprt get_free_function()
Get the free function as symbol expression, and inserts it into the goto-model if it doesn't exist al...
Definition: recursive_initialization.cpp:599
harness_options_parser::require_one_size_value
std::size_t require_one_size_value(const std::string &option, const std::list< std::string > &values)
Returns the only Nat value of a single element list, throws an exception if not passed a single eleme...
Definition: goto_harness_generator.cpp:41
goto_modelt::get_symbol_table
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:77
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
code_typet::parametert
Definition: std_types.h:753
recursive_initialization_configt
Definition: recursive_initialization.h:26
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
recursive_initialization_configt::min_null_tree_depth
std::size_t min_null_tree_depth
Definition: recursive_initialization.h:27
recursive_initializationt::equal_cluster_idt
std::size_t equal_cluster_idt
Definition: recursive_initialization.h:65
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
recursive_initializationt::build_nondet_constructor
code_blockt build_nondet_constructor(const symbol_exprt &result) const
Default constructor: assigns non-deterministic value of the right type.
Definition: recursive_initialization.cpp:769
r
static int8_t r
Definition: irep_hash.h:59
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT
#define COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT
Definition: common_harness_generator_options.h:12
index_exprt
Array index operator.
Definition: std_expr.h:1299
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2815
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
Definition: common_harness_generator_options.h:16
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:298
recursive_initialization_configt::to_string
std::string to_string() const
Definition: recursive_initialization.cpp:421
recursive_initializationt::initialization_config
const recursive_initialization_configt initialization_config
Definition: recursive_initialization.h:118
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
std_expr.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
allocate_objects.h
c_types.h
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
recursive_initializationt::max_depth_var_name
irep_idt max_depth_var_name
Definition: recursive_initialization.h:120
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1876
irep.h
recursive_initialization_configt::pointers_to_treat_equal
std::vector< std::set< irep_idt > > pointers_to_treat_equal
Definition: recursive_initialization.h:41
recursive_initializationt::build_struct_constructor
code_blockt build_struct_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for structures: simply iterates over members and initialise each one.
Definition: recursive_initialization.cpp:752
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3968