Minimize our macro definitions for CBMC proofs #706
Labels
cbmc
Anything related to CBMC proofs.
needs-review
This issue or pull request needs review from a core team member.
p3
This is a minor priority issue
In some proofs we use
ASSUME_VALID_MEMORY_COUNT
to properly allocate a valid memory in proof harnesses.It's nice to have a new macro that does the malloc + the nullness etc. checks, but we are introducing yet another macro and would have to remember to use it consistently across the preconditions and harness assumptions etc.
We should take a pass and minimize our macro definitions at some point. Otherwise, let's make consistently.
The text was updated successfully, but these errors were encountered: