Skip to content

Assigns clause should only check assignments over variables from the write set #6154

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
feliperodri opened this issue May 26, 2021 · 1 comment · Fixed by #6279
Closed

Assigns clause should only check assignments over variables from the write set #6154

feliperodri opened this issue May 26, 2021 · 1 comment · Fixed by #6279
Assignees
@feliperodri
Labels
aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts enhancement

Comments

@feliperodri
Copy link
Collaborator

CBMC version: develop branch.
Operating system: N/A.
Exact command line resulting in the issue: N/A.
What behaviour did you expect: We only want to check assignments over variables from the write set. Local variables should be ignored.
What happened instead: When using assigns clause, CBMC checks for all assignments, even if they are over local variables.
@feliperodri feliperodri added enhancement aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels May 26, 2021
@feliperodri feliperodri self-assigned this May 26, 2021
@feliperodri feliperodri mentioned this issue May 26, 2021
Merged
7 tasks
@SaswatPadhi
Copy link
Contributor

Context: #6108 (comment)

@SaswatPadhi SaswatPadhi mentioned this issue Aug 8, 2021
Merged
7 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@feliperodri feliperodri

Labels
aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts enhancement
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Skip checking frame conditions for local variables feliperodri/cbmc
2 participants
@SaswatPadhi @feliperodri