cprover
remove_const_function_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs
4 
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/arith_tools.h>
15 #include <util/format_expr.h>
16 #include <util/simplify_expr.h>
17 #include <util/std_expr.h>
18 #include <util/symbol_table.h>
19 
20 #include "goto_functions.h"
21 
22 #define LOG(message, irep) \
23  do { \
24  debug().source_location = irep.source_location(); \
25  debug() << message << ": " << format(irep) << eom; \
26  } \
27  while(0)
28 
35  message_handlert &message_handler,
36  const namespacet &ns,
37  const symbol_tablet &symbol_table):
38  messaget(message_handler),
39  ns(ns),
40  symbol_table(symbol_table)
41 {}
42 
55  const exprt &base_expression,
56  functionst &out_functions)
57 {
58  // Replace all const symbols with their values
59  exprt non_symbol_expression=replace_const_symbols(base_expression);
60  return try_resolve_function_call(non_symbol_expression, out_functions);
61 }
62 
71  const exprt &expression) const
72 {
73  if(expression.id()==ID_symbol)
74  {
75  if(is_const_expression(expression))
76  {
77  const symbolt &symbol =
78  symbol_table.lookup_ref(to_symbol_expr(expression).get_identifier());
79  if(symbol.type.id()!=ID_code)
80  {
81  const exprt &symbol_value=symbol.value;
82  return replace_const_symbols(symbol_value);
83  }
84  else
85  {
86  return expression;
87  }
88  }
89  else
90  {
91  return expression;
92  }
93  }
94  else
95  {
96  exprt const_symbol_cleared_expr=expression;
97  const_symbol_cleared_expr.operands().clear();
98  for(const exprt &op : expression.operands())
99  {
100  exprt const_symbol_cleared_op=replace_const_symbols(op);
101  const_symbol_cleared_expr.operands().push_back(const_symbol_cleared_op);
102  }
103 
104  return const_symbol_cleared_expr;
105  }
106 }
107 
112  const symbol_exprt &symbol_expr) const
113 {
114  const symbolt &symbol = symbol_table.lookup_ref(symbol_expr.get_identifier());
115  return symbol.value;
116 }
117 
127  const exprt &expr, functionst &out_functions)
128 {
129  PRECONDITION(out_functions.empty());
130  const exprt &simplified_expr=simplify_expr(expr, ns);
131  bool resolved=false;
132  functionst resolved_functions;
133  if(simplified_expr.id()==ID_index)
134  {
135  const index_exprt &index_expr=to_index_expr(simplified_expr);
136  resolved=try_resolve_index_of_function_call(index_expr, resolved_functions);
137  }
138  else if(simplified_expr.id()==ID_member)
139  {
140  const member_exprt &member_expr=to_member_expr(simplified_expr);
141  resolved=try_resolve_member_function_call(member_expr, resolved_functions);
142  }
143  else if(simplified_expr.id()==ID_address_of)
144  {
145  address_of_exprt address_expr=to_address_of_expr(simplified_expr);
147  address_expr, resolved_functions);
148  }
149  else if(simplified_expr.id()==ID_dereference)
150  {
151  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
152  resolved=try_resolve_dereference_function_call(deref, resolved_functions);
153  }
154  else if(simplified_expr.id()==ID_typecast)
155  {
156  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
157  resolved=
158  try_resolve_typecast_function_call(typecast_expr, resolved_functions);
159  }
160  else if(simplified_expr.id()==ID_symbol)
161  {
162  if(simplified_expr.type().id()==ID_code)
163  {
164  resolved_functions.insert(to_symbol_expr(simplified_expr));
165  resolved=true;
166  }
167  else
168  {
169  LOG("Non const symbol wasn't squashed", simplified_expr);
170  resolved=false;
171  }
172  }
173  else if(simplified_expr.id()==ID_constant)
174  {
175  if(simplified_expr.is_zero())
176  {
177  // We have the null pointer - no need to throw everything away
178  // but we don't add any functions either
179  resolved=true;
180  }
181  else
182  {
183  LOG("Non-zero constant value found", simplified_expr);
184  resolved=false;
185  }
186  }
187  else
188  {
189  LOG("Unrecognised expression", simplified_expr);
190  resolved=false;
191  }
192 
193  if(resolved)
194  {
195  out_functions.insert(resolved_functions.begin(), resolved_functions.end());
196  return true;
197  }
198  else
199  {
200  return false;
201  }
202 }
203 
211  const expressionst &exprs, functionst &out_functions)
212 {
213  for(const exprt &value : exprs)
214  {
215  functionst potential_out_functions;
216  bool resolved_value=
217  try_resolve_function_call(value, potential_out_functions);
218 
219  if(resolved_value)
220  {
221  out_functions.insert(
222  potential_out_functions.begin(),
223  potential_out_functions.end());
224  }
225  else
226  {
227  LOG("Could not resolve expression in array", value);
228  return false;
229  }
230  }
231  return true;
232 }
233 
246  const index_exprt &index_expr, functionst &out_functions)
247 {
248  expressionst potential_array_values;
249  bool array_const;
250  bool resolved=
251  try_resolve_index_of(index_expr, potential_array_values, array_const);
252 
253  if(!resolved)
254  {
255  LOG("Could not resolve array", index_expr);
256  return false;
257  }
258 
259  if(!array_const)
260  {
261  LOG("Array not const", index_expr);
262  return false;
263  }
264 
265  return try_resolve_function_calls(potential_array_values, out_functions);
266 }
267 
278  const member_exprt &member_expr, functionst &out_functions)
279 {
280  expressionst potential_component_values;
281  bool struct_const;
282  bool resolved=
283  try_resolve_member(member_expr, potential_component_values, struct_const);
284 
285  if(!resolved)
286  {
287  LOG("Could not resolve struct", member_expr);
288  return false;
289  }
290 
291  if(!struct_const)
292  {
293  LOG("Struct was not const so can't resolve values on it", member_expr);
294  return false;
295  }
296 
297  return try_resolve_function_calls(potential_component_values, out_functions);
298 }
299 
309  const address_of_exprt &address_expr, functionst &out_functions)
310 {
311  bool resolved=
312  try_resolve_function_call(address_expr.object(), out_functions);
313  if(!resolved)
314  {
315  LOG("Failed to resolve address of", address_expr);
316  }
317  return resolved;
318 }
319 
330  const dereference_exprt &deref_expr, functionst &out_functions)
331 {
332  expressionst potential_deref_values;
333  bool deref_const;
334  bool resolved=
335  try_resolve_dereference(deref_expr, potential_deref_values, deref_const);
336 
337  if(!resolved)
338  {
339  LOG("Failed to squash dereference", deref_expr);
340  return false;
341  }
342 
343  if(!deref_const)
344  {
345  LOG("Dereferenced value was not const so can't dereference", deref_expr);
346  return false;
347  }
348 
349  return try_resolve_function_calls(potential_deref_values, out_functions);
350 }
351 
362  const typecast_exprt &typecast_expr, functionst &out_functions)
363 {
364  // We simply ignore typecasts and assume they are valid
365  // I thought simplify_expr would deal with this, but for example
366  // a cast from a 32 bit width int to a 64bit width int it doesn't seem
367  // to allow
368  functionst typecast_values;
369  bool resolved=
370  try_resolve_function_call(typecast_expr.op(), typecast_values);
371 
372  if(resolved)
373  {
374  out_functions.insert(typecast_values.begin(), typecast_values.end());
375  return true;
376  }
377  else
378  {
379  LOG("Failed to squash typecast", typecast_expr);
380  return false;
381  }
382 }
383 
399  const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
400 {
401  exprt simplified_expr=simplify_expr(expr, ns);
402  bool resolved;
403  expressionst resolved_expressions;
404  bool is_resolved_expression_const = false;
405  if(simplified_expr.id()==ID_index)
406  {
407  const index_exprt &index_expr=to_index_expr(simplified_expr);
408  resolved=
410  index_expr, resolved_expressions, is_resolved_expression_const);
411  }
412  else if(simplified_expr.id()==ID_member)
413  {
414  const member_exprt &member_expr=to_member_expr(simplified_expr);
415  resolved=try_resolve_member(
416  member_expr, resolved_expressions, is_resolved_expression_const);
417  }
418  else if(simplified_expr.id()==ID_dereference)
419  {
420  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
421  resolved=
423  deref, resolved_expressions, is_resolved_expression_const);
424  }
425  else if(simplified_expr.id()==ID_typecast)
426  {
427  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
428  resolved=
430  typecast_expr, resolved_expressions, is_resolved_expression_const);
431  }
432  else if(simplified_expr.id()==ID_symbol)
433  {
434  LOG("Non const symbol will not be squashed", simplified_expr);
435  resolved=false;
436  }
437  else
438  {
439  resolved_expressions.push_back(simplified_expr);
440  is_resolved_expression_const=is_const_expression(simplified_expr);
441  resolved=true;
442  }
443 
444  if(resolved)
445  {
446  out_resolved_expression.insert(
447  out_resolved_expression.end(),
448  resolved_expressions.begin(),
449  resolved_expressions.end());
450  out_is_const=is_resolved_expression_const;
451  return true;
452  }
453  else
454  {
455  return false;
456  }
457 }
458 
468  const exprt &expr, mp_integer &out_array_index)
469 {
470  expressionst index_value_expressions;
471  bool is_const=false;
472  bool resolved=try_resolve_expression(expr, index_value_expressions, is_const);
473  if(resolved)
474  {
475  if(index_value_expressions.size()==1 &&
476  index_value_expressions.front().id()==ID_constant)
477  {
478  const constant_exprt &constant_expr=
479  to_constant_expr(index_value_expressions.front());
480  mp_integer array_index;
481  bool errors=to_integer(constant_expr, array_index);
482  if(!errors)
483  {
484  out_array_index=array_index;
485  }
486  return !errors;
487  }
488  else
489  {
490  return false;
491  }
492  }
493  else
494  {
495  return false;
496  }
497 }
498 
510  const index_exprt &index_expr,
511  expressionst &out_expressions,
512  bool &out_is_const)
513 {
514  // Get the array(s) it belongs to
515  expressionst potential_array_exprs;
516  bool array_const=false;
517  bool resolved_array=
519  index_expr.array(),
520  potential_array_exprs,
521  array_const);
522 
523  if(resolved_array)
524  {
525  bool all_possible_const=true;
526  for(const exprt &potential_array_expr : potential_array_exprs)
527  {
528  all_possible_const=
529  all_possible_const &&
530  is_const_type(potential_array_expr.type().subtype());
531 
532  if(potential_array_expr.id()==ID_array)
533  {
534  // Get the index if we can
535  mp_integer value;
536  if(try_resolve_index_value(index_expr.index(), value))
537  {
538  expressionst array_out_functions;
539  const exprt &func_expr =
540  potential_array_expr.operands()[numeric_cast_v<std::size_t>(value)];
541  bool value_const=false;
542  bool resolved_value=
543  try_resolve_expression(func_expr, array_out_functions, value_const);
544 
545  if(resolved_value)
546  {
547  out_expressions.insert(
548  out_expressions.end(),
549  array_out_functions.begin(),
550  array_out_functions.end());
551  }
552  else
553  {
554  LOG("Failed to resolve array value", func_expr);
555  return false;
556  }
557  }
558  else
559  {
560  // We don't know what index it is,
561  // but we know the value is from the array
562  for(const exprt &array_entry : potential_array_expr.operands())
563  {
564  expressionst array_contents;
565  bool is_entry_const;
566  bool resolved_value=
568  array_entry, array_contents, is_entry_const);
569 
570  if(!resolved_value)
571  {
572  LOG("Failed to resolve array value", array_entry);
573  return false;
574  }
575 
576  for(const exprt &resolved_array_entry : array_contents)
577  {
578  out_expressions.push_back(resolved_array_entry);
579  }
580  }
581  }
582  }
583  else
584  {
585  LOG(
586  "Squashing index of did not result in an array",
587  potential_array_expr);
588  return false;
589  }
590  }
591 
592  out_is_const=all_possible_const || array_const;
593  return true;
594  }
595  else
596  {
597  LOG("Failed to squash index of to array expression", index_expr);
598  return false;
599  }
600 }
601 
611  const member_exprt &member_expr,
612  expressionst &out_expressions,
613  bool &out_is_const)
614 {
615  expressionst potential_structs;
616  bool is_struct_const;
617 
618  // Get the struct it belongs to
619  bool resolved_struct=
621  member_expr.compound(), potential_structs, is_struct_const);
622  if(resolved_struct)
623  {
624  for(const exprt &potential_struct : potential_structs)
625  {
626  if(potential_struct.id()==ID_struct)
627  {
628  struct_exprt struct_expr=to_struct_expr(potential_struct);
629  const exprt &component_value=
630  get_component_value(struct_expr, member_expr);
631  expressionst resolved_expressions;
632  bool component_const=false;
633  bool resolved=
635  component_value, resolved_expressions, component_const);
636  if(resolved)
637  {
638  out_expressions.insert(
639  out_expressions.end(),
640  resolved_expressions.begin(),
641  resolved_expressions.end());
642  }
643  else
644  {
645  LOG("Could not resolve component value", component_value);
646  return false;
647  }
648  }
649  else
650  {
651  LOG(
652  "Squashing member access did not resolve in a struct",
653  potential_struct);
654  return false;
655  }
656  }
657  out_is_const=is_struct_const;
658  return true;
659  }
660  else
661  {
662  LOG("Failed to squash struct access", member_expr);
663  return false;
664  }
665 }
666 
678  const dereference_exprt &deref_expr,
679  expressionst &out_expressions,
680  bool &out_is_const)
681 {
682  // We had a pointer, we need to check both the pointer
683  // type can't be changed, and what it what pointing to
684  // can't be changed
685  expressionst pointer_values;
686  bool pointer_const;
687  bool resolved=
688  try_resolve_expression(deref_expr.pointer(), pointer_values, pointer_const);
689  if(resolved && pointer_const)
690  {
691  bool all_objects_const=true;
692  for(const exprt &pointer_val : pointer_values)
693  {
694  if(pointer_val.id()==ID_address_of)
695  {
696  address_of_exprt address_expr=to_address_of_expr(pointer_val);
697  bool object_const=false;
698  expressionst out_object_values;
699  const bool resolved_address = try_resolve_expression(
700  address_expr.object(), out_object_values, object_const);
701 
702  if(resolved_address)
703  {
704  out_expressions.insert(
705  out_expressions.end(),
706  out_object_values.begin(),
707  out_object_values.end());
708 
709  all_objects_const&=object_const;
710  }
711  else
712  {
713  LOG("Failed to resolve value of a dereference", address_expr);
714  }
715  }
716  else
717  {
718  LOG(
719  "Squashing dereference did not result in an address", pointer_val);
720  return false;
721  }
722  }
723  out_is_const=all_objects_const;
724  return true;
725  }
726  else
727  {
728  if(!resolved)
729  {
730  LOG("Failed to resolve pointer of dereference", deref_expr);
731  }
732  else if(!pointer_const)
733  {
734  LOG("Pointer value not const so can't squash", deref_expr);
735  }
736  return false;
737  }
738 }
739 
748  const typecast_exprt &typecast_expr,
749  expressionst &out_expressions,
750  bool &out_is_const)
751 {
752  expressionst typecast_values;
753  bool typecast_const;
754  bool resolved=
756  typecast_expr.op(), typecast_values, typecast_const);
757 
758  if(resolved)
759  {
760  out_expressions.insert(
761  out_expressions.end(),
762  typecast_values.begin(),
763  typecast_values.end());
764  out_is_const=typecast_const;
765  return true;
766  }
767  else
768  {
769  LOG("Could not resolve typecast value", typecast_expr);
770  return false;
771  }
772 }
773 
778  const exprt &expression) const
779 {
780  return is_const_type(expression.type());
781 }
782 
788 {
789  if(type.id() == ID_array && type.subtype().get_bool(ID_C_constant))
790  return true;
791 
792  return type.get_bool(ID_C_constant);
793 }
794 
801  const struct_exprt &struct_expr, const member_exprt &member_expr)
802 {
803  const struct_typet &struct_type=to_struct_type(ns.follow(struct_expr.type()));
804  size_t component_number=
805  struct_type.component_number(member_expr.get_component_name());
806 
807  return struct_expr.operands()[component_number];
808 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
remove_const_function_pointerst::operator()
bool operator()(const exprt &base_expression, functionst &out_functions)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
Definition: remove_const_function_pointers.cpp:54
remove_const_function_pointerst::try_resolve_typecast
bool try_resolve_typecast(const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
To squash a typecast access.
Definition: remove_const_function_pointers.cpp:747
remove_const_function_pointerst::try_resolve_member
bool try_resolve_member(const member_exprt &member_expr, expressionst &out_expressions, bool &out_is_const)
To squash an member access by first finding the struct it is accessing Then return the squashed value...
Definition: remove_const_function_pointers.cpp:610
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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
remove_const_function_pointerst::try_resolve_dereference_function_call
bool try_resolve_dereference_function_call(const dereference_exprt &deref_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
Definition: remove_const_function_pointers.cpp:329
typet::subtype
const typet & subtype() const
Definition: type.h:47
remove_const_function_pointerst::is_const_expression
bool is_const_expression(const exprt &expression) const
To evaluate the const-ness of the expression type.
Definition: remove_const_function_pointers.cpp:777
remove_const_function_pointerst::try_resolve_dereference
bool try_resolve_dereference(const dereference_exprt &deref_expr, expressionst &out_expressions, bool &out_is_const)
To squash a dereference access by first finding the address_of the dereference is dereferencing.
Definition: remove_const_function_pointers.cpp:677
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
typet
The type of an expression, extends irept.
Definition: type.h:29
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
remove_const_function_pointerst::try_resolve_function_calls
bool try_resolve_function_calls(const expressionst &exprs, functionst &out_functions)
To resolve a collection of expressions to the specific function calls they can be.
Definition: remove_const_function_pointers.cpp:210
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
remove_const_function_pointerst::replace_const_symbols
exprt replace_const_symbols(const exprt &expression) const
To collapse the symbols down to their values where possible This takes a very general approach,...
Definition: remove_const_function_pointers.cpp:70
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
remove_const_function_pointerst::try_resolve_function_call
bool try_resolve_function_call(const exprt &expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
Definition: remove_const_function_pointers.cpp:126
remove_const_function_pointerst::try_resolve_expression
bool try_resolve_expression(const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
To squash various expr types to simplify the expression.
Definition: remove_const_function_pointers.cpp:398
remove_const_function_pointerst::try_resolve_index_of_function_call
bool try_resolve_index_of_function_call(const index_exprt &index_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
Definition: remove_const_function_pointers.cpp:245
exprt
Base class for all expressions.
Definition: expr.h:53
remove_const_function_pointerst::symbol_table
const symbol_tablet & symbol_table
Definition: remove_const_function_pointers.h:105
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
remove_const_function_pointerst::is_const_type
bool is_const_type(const typet &type) const
To evaluate the const-ness of the type.
Definition: remove_const_function_pointers.cpp:787
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
struct_union_typet::component_number
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:36
remove_const_function_pointerst::functionst
std::unordered_set< symbol_exprt, irep_hash > functionst
Definition: remove_const_function_pointers.h:35
remove_const_function_pointerst::get_component_value
exprt get_component_value(const struct_exprt &struct_expr, const member_exprt &member_expr)
To extract the value of the specific component within a struct.
Definition: remove_const_function_pointers.cpp:800
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
remove_const_function_pointerst::ns
const namespacet & ns
Definition: remove_const_function_pointers.h:104
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3446
remove_const_function_pointerst::try_resolve_index_of
bool try_resolve_index_of(const index_exprt &index_expr, expressionst &out_expressions, bool &out_is_const)
To squash an index access by first finding the array it is accessing Then if the index can be resolve...
Definition: remove_const_function_pointers.cpp:509
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
remove_const_function_pointerst::try_resolve_typecast_function_call
bool try_resolve_typecast_function_call(const typecast_exprt &typecast_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
Definition: remove_const_function_pointers.cpp:361
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
remove_const_function_pointerst::try_resolve_index_value
bool try_resolve_index_value(const exprt &index_value_expr, mp_integer &out_array_index)
Given an index into an array, resolve, if possible, the index that is being accessed.
Definition: remove_const_function_pointers.cpp:467
remove_const_function_pointerst::expressionst
std::list< exprt > expressionst
Definition: remove_const_function_pointers.h:36
simplify_expr.h
remove_const_function_pointerst::try_resolve_member_function_call
bool try_resolve_member_function_call(const member_exprt &member_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
Definition: remove_const_function_pointers.cpp:277
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
format_expr.h
remove_const_function_pointers.h
Goto Programs.
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
goto_functions.h
Goto Programs with Functions.
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
remove_const_function_pointerst::resolve_symbol
exprt resolve_symbol(const symbol_exprt &symbol_expr) const
Look up a symbol in the symbol table and return its value.
Definition: remove_const_function_pointers.cpp:111
exprt::operands
operandst & operands()
Definition: expr.h:95
remove_const_function_pointerst::remove_const_function_pointerst
remove_const_function_pointerst(message_handlert &message_handler, const namespacet &ns, const symbol_tablet &symbol_table)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
Definition: remove_const_function_pointers.cpp:34
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
std_expr.h
API to expression classes.
remove_const_function_pointerst::try_resolve_address_of_function_call
bool try_resolve_address_of_function_call(const address_of_exprt &address_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
Definition: remove_const_function_pointers.cpp:308
LOG
#define LOG(message, irep)
Definition: remove_const_function_pointers.cpp:22
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939