Skip to content

Commit 471dca7

Browse files
Factor handling the base case out of dereference
1 parent 0eb945d commit 471dca7

File tree

2 files changed

+10
-1
lines changed

2 files changed

+10
-1
lines changed

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,13 @@ exprt value_set_dereferencet::dereference(
141141
}
142142
}
143143

144-
// type of the object
144+
return handle_dereference_base_case(pointer, display_points_to_sets);
145+
}
146+
147+
exprt value_set_dereferencet::handle_dereference_base_case(
148+
const exprt &pointer,
149+
bool display_points_to_sets)
150+
{ // type of the object
145151
const typet &type=pointer.type().subtype();
146152

147153
// collect objects the pointer may point to

src/pointer-analysis/value_set_dereference.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,9 @@ class value_set_dereferencet final
112112
const bool exclude_null_derefs;
113113
const messaget &log;
114114
valuet get_failure_value(const exprt &pointer, const typet &type);
115+
exprt handle_dereference_base_case(
116+
const exprt &pointer,
117+
bool display_points_to_sets);
115118
};
116119

117120
#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H

0 commit comments

Comments
 (0)