Investigate how to move assumptions out of ensure_...
functions
#675
Labels
cbmc
CBMC proof related work
ensure_...
functions
#675
Some
ensure_...
functions need to make assumptions about certain sub-structures before doing the regular "ensuring" process. We will investigate ways to move these assumptions somewhere else or remove them completely.As an example, the function
ensure_default_cmm_attempt_allocation
from #656 where the following code is executed before allocatingcmm
:The text was updated successfully, but these errors were encountered: