Skip to content

Commit bb73e61

Browse files
committed
Improve comments and fix invariant message
that was not up-to-date.
1 parent 859c83a commit bb73e61

File tree

2 files changed

+7
-4
lines changed

2 files changed

+7
-4
lines changed

src/goto-programs/remove_function_pointers.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -150,9 +150,12 @@ class remove_function_pointerst
150150
/// if (fp=&f1) then goto loc1
151151
/// if (fp=&f2) then goto loc2
152152
/// ..
153-
/// loc1: f1(); goto N+1;
154-
/// loc2: f2(); goto N+1;
153+
/// if (fp=&fn) then goto locN
154+
/// loc1: f1(); goto N+1;
155+
/// loc2: f2(); goto N+1;
155156
/// ..
157+
/// locN: fn(); goto N+1;
158+
/// locN+1:
156159
///
157160
/// \param functions: set of function candidates
158161
/// \param code: the original function call

src/goto-programs/remove_returns.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -196,8 +196,8 @@ bool remove_returnst::do_function_calls(
196196
INVARIANT(
197197
function_call.function().id() == ID_symbol ||
198198
function_call.function().id() == ID_dereference,
199-
"indirect function calls should have been removed prior to running "
200-
"remove-returns");
199+
"only direct function calls (via a symbol) or indirect function calls "
200+
"(via a dereference) are supported");
201201

202202
bool is_function_pointer = function_call.function().id() == ID_dereference;
203203

0 commit comments

Comments
 (0)