cprover
value_set_dereference.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pointer Dereferencing
4
5Author: 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
18class messaget;
19class symbol_tablet;
20
23{
24public:
32 // given dereference may follow a null pointer
35 const namespacet &_ns,
36 symbol_tablet &_new_symbol_table,
37 dereference_callbackt &_dereference_callback,
38 const irep_idt _language_mode,
39 bool _exclude_null_derefs,
40 const messaget &_log)
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 log(_log)
47 { }
48
50
55 exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
56
61 try_add_offset_to_indices(const exprt &expr, const exprt &offset);
62
64 class valuet
65 {
66 public:
70
73 {
74 }
75 };
76
77 static bool should_ignore_value(
78 const exprt &what,
80 const irep_idt &language_mode);
81
82 static valuet build_reference_to(
83 const exprt &what,
84 const exprt &pointer,
85 const namespacet &ns);
86
87 static bool dereference_type_compare(
88 const typet &object_type,
89 const typet &dereference_type,
90 const namespacet &ns);
91
92 static bool memory_model(
93 exprt &value,
94 const typet &type,
95 const exprt &offset,
96 const namespacet &ns);
97
98 static bool memory_model_bytes(
99 exprt &value,
100 const typet &type,
101 const exprt &offset,
102 const namespacet &ns);
103
104private:
114 const messaget &log;
115 valuet get_failure_value(const exprt &pointer, const typet &type);
117 const exprt &pointer,
118 bool display_points_to_sets);
119};
120
121#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:37
Base class for all expressions.
Definition: expr.h:54
The Boolean constant false.
Definition: std_expr.h:2865
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
The symbol table.
Definition: symbol_table.h:14
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)
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs, const messaget &_log)
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
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...
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)
optionalt< exprt > try_add_offset_to_indices(const exprt &expr, const exprt &offset)
If expr is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) then return c1 ? e1[o1 + offset] : e2[o...
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...
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes.