CBMC
value_set_dereference.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Dereferencing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
14 
15 #include <util/std_expr.h>
16 
18 class message_handlert;
19 class symbol_table_baset;
20 
23 {
24 public:
32  // given dereference may follow a null pointer
35  const namespacet &_ns,
36  symbol_table_baset &_new_symbol_table,
37  dereference_callbackt &_dereference_callback,
38  const irep_idt _language_mode,
39  bool _exclude_null_derefs,
40  message_handlert &_message_handler)
41  : ns(_ns),
42  new_symbol_table(_new_symbol_table),
43  dereference_callback(_dereference_callback),
44  language_mode(_language_mode),
45  exclude_null_derefs(_exclude_null_derefs),
46  message_handler(_message_handler)
47  { }
48 
50 
55  exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
56 
58  class valuet
59  {
60  public:
64 
67  {
68  }
69  };
70 
71  static bool should_ignore_value(
72  const exprt &what,
74  const irep_idt &language_mode);
75 
76  static valuet build_reference_to(
77  const exprt &what,
78  const exprt &pointer,
79  const namespacet &ns);
80 
81  static bool dereference_type_compare(
82  const typet &object_type,
83  const typet &dereference_type,
84  const namespacet &ns);
85 
86  static bool memory_model(
87  exprt &value,
88  const typet &type,
89  const exprt &offset,
90  const namespacet &ns);
91 
92  static bool memory_model_bytes(
93  exprt &value,
94  const typet &type,
95  const exprt &offset,
96  const namespacet &ns);
97 
98 private:
99  const namespacet &ns;
109  valuet get_failure_value(const exprt &pointer, const typet &type);
111  const exprt &pointer,
112  bool display_points_to_sets);
113 };
114 
115 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
Base class for pointer value set analysis.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
The Boolean constant false.
Definition: std_expr.h:3077
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3086
The symbol table base class interface.
The type of an expression, extends irept.
Definition: type.h:29
Return value for build_reference_to; see that method for documentation.
Wrapper for a function dereferencing pointer expressions using a value set.
static bool memory_model_bytes(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
valuet get_failure_value(const exprt &pointer, const typet &type)
exprt handle_dereference_base_case(const exprt &pointer, bool display_points_to_sets)
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
symbol_table_baset & new_symbol_table
static bool dereference_type_compare(const typet &object_type, const typet &dereference_type, const namespacet &ns)
Check if the two types have matching number of ID_pointer levels, with the dereference type eventuall...
value_set_dereferencet(const namespacet &_ns, symbol_table_baset &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs, message_handlert &_message_handler)
message_handlert & message_handler
dereference_callbackt & dereference_callback
exprt dereference(const exprt &pointer, bool display_points_to_sets=false)
Dereference the given pointer-expression.
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
static bool memory_model(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
API to expression classes.