-
Notifications
You must be signed in to change notification settings - Fork 277
Open
Labels
awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersenhancement
Description
Because __CPROVER_allocated_memory
is currently flow insensitive, multiple instances of this intrinsic for the same hardware style memory address should be considered invalid input to cbmc, because that is introducing conflicting specifications of how much memory is allocated. cbmc
should check for and reject this type of input.
Additional kinds of checks on this intrinsic/allocation which we should add in order to help ensure our model of hardware memory allocation is sound -
- Checks on duplicate/overlapping allocation definitions for the same address.
- Checks that allocated address and the size of the allocation are constants.
- Potentially, a "reasonable" limit on the maximum size of an allocation.
Metadata
Metadata
Assignees
Labels
awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersenhancement