Skip to content

Improve check_for_looped_mallocs in code contracts to use natural loops #5530

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 Oct 15, 2020 · 2 comments · Fixed by #6729
Closed

Improve check_for_looped_mallocs in code contracts to use natural loops #5530

feliperodri opened this issue Oct 15, 2020 · 2 comments · Fixed by #6729
Assignees
@feliperodri
Labels
aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts

Comments

@feliperodri
Copy link
Collaborator

CBMC version: >5.15
Operating system: Ubuntu 18.04 or macOS Mojave 10.14.6
Exact command line resulting in the issue: N/A.
What behaviour did you expect: N/A.
What happened instead: Use natural_loops, as is done, e.g., in dump_c. That will directly provide you with a loop body, which can then be searched for those function calls.

Suggested in #5403.
@feliperodri feliperodri added the aws Bugs or features of importance to AWS CBMC users label Oct 15, 2020
@feliperodri feliperodri changed the title Improve check_for_looped_mallocs in code contracts to use natrual loops Improve check_for_looped_mallocs in code contracts to use natural loops Oct 15, 2020
@feliperodri feliperodri mentioned this issue Oct 15, 2020
Merged
7 tasks
@feliperodri feliperodri added the Code Contracts Function and loop contracts label Feb 5, 2021
@feliperodri feliperodri self-assigned this Feb 5, 2021
@feliperodri
Copy link
Collaborator Author

feliperodri commented Jul 20, 2021 •
edited
Loading

We should only update checked_for_looped_malloc once issue #6168 is resolved.

@jimgrundy jimgrundy changed the title Improve check_for_looped_mallocs in code contracts to use natural loops Improve check_for_looped_mallocs in code contracts to use natural loops [depends-on #6168] Aug 24, 2021
@SaswatPadhi
Copy link
Contributor

#6168 is now resolved and the fix has been merged, so may be we can take another look at this issue now.

@SaswatPadhi SaswatPadhi changed the title Improve check_for_looped_mallocs in code contracts to use natural loops [depends-on #6168] Improve check_for_looped_mallocs in code contracts to use natural loops Sep 22, 2021
@feliperodri feliperodri mentioned this issue Mar 14, 2022
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
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

CONTRACTS: Remove helper method check_for_looped_mallocs feliperodri/cbmc
2 participants
@SaswatPadhi @feliperodri