Skip to content

Commit 06a68ec

Browse files
committed
Document remove_unused_functions dependency on remove_function_pointers
1 parent f4f9a30 commit 06a68ec

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

doc/architectural/goto-program-transformations.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -282,6 +282,11 @@ This pass removes unused functions from the goto model. In practice this builds
282282
a collection of all the functions that are potentially called, and then removes
283283
any function not in this collection.
284284

285+
This pass cannot handle function calls via function pointers. Attempting to run
286+
this pass against a goto model which contains such a function call will result
287+
in an invariant violation. Therefore the function pointer removal pass must
288+
always be applied to the goto model before the remove unused functions pass.
289+
285290
The implementation of this pass is called via the \ref
286291
remove_unused_functions(goto_modelt &, message_handlert &) function.
287292

0 commit comments

Comments
 (0)