Description
CBMC version: 516f109
Operating system: n/a
Exact command line resulting in the issue: n/a (internal code refactor)
What behaviour did you expect: n/a (internal code refactor)
What happened instead: n/a (internal code refactor)
Related to @tautschnig's comment on a recent PR: #6249 (comment)
There are several methods and classes in goto-instrument that implement "assigns" (i.e., "writes") semantics but are named "modifies*" (e.g., get_modifies method in loop_utils.h, function_modifiest class in function_modifies.h etc.) We should refactor these and rename them to "assigns*" to avoid any possible confusion in the future. x := x is a non-modifying write.
The function_modifiest member function implementations also look quite similar to methods within loop_utils.cpp. We should also look into unifying these implementations.