Skip to content

Rename "modifies*" entities in order to avoid possible confusion #6467

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
SaswatPadhi opened this issue Nov 19, 2021 · 0 comments · Fixed by #6504
Closed

Rename "modifies*" entities in order to avoid possible confusion #6467

SaswatPadhi opened this issue Nov 19, 2021 · 0 comments · Fixed by #6504
Assignees
@tautschnig @remi-delmas-3000 @feliperodri
Labels
aws Bugs or features of importance to AWS CBMC users cleanup pending merge

Comments

@SaswatPadhi
Copy link
Contributor

SaswatPadhi commented Nov 19, 2021 •
edited
Loading

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.
@SaswatPadhi SaswatPadhi added cleanup aws Bugs or features of importance to AWS CBMC users labels Nov 19, 2021
@SaswatPadhi SaswatPadhi mentioned this issue Nov 19, 2021
Merged
5 tasks
tautschnig added a commit to tautschnig/cbmc that referenced this issue Dec 4, 2021
@tautschnig
goto-instrument: replace "modifies" by "assigns" terminology
52828db 
All this code collects assignments rather than checking for genuine
value changes (modifications).

Fixes: diffblue#6467
@tautschnig tautschnig mentioned this issue Dec 4, 2021
Merged
4 tasks
tautschnig added a commit to tautschnig/cbmc that referenced this issue Dec 6, 2021
@tautschnig
goto-instrument: replace "modifies" by "assigns" terminology
84d272f 
All this code collects assignments rather than checking for genuine
value changes (modifications).

Fixes: diffblue#6467
vmihalko pushed a commit to vmihalko/cbmc that referenced this issue Jan 24, 2022
@tautschnig @vmihalko
goto-instrument: replace "modifies" by "assigns" terminology
ab10800 
All this code collects assignments rather than checking for genuine
value changes (modifications).

Fixes: diffblue#6467
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@tautschnig tautschnig

@remi-delmas-3000 remi-delmas-3000

@feliperodri feliperodri

Labels
aws Bugs or features of importance to AWS CBMC users cleanup pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

goto-instrument: replace "modifies" by "assigns" terminology tautschnig/cbmc
4 participants
@tautschnig @SaswatPadhi @remi-delmas-3000 @feliperodri