Motivation
Currently, we only have one bookkeeping variable $Alloc for the entire program. We can split it into multiple bookkeep variables such that one variable roughly corresponds to one allocation site (i.e., a call to malloc or an alloca instruction). Having multiple bookkeeping variables reduces the solver's burden to reason about arrays.
Implementation Plan
The key idea to implement this feature is to id allocation sites and find out which allocate sites a pointer is associated with.
However, an implication of having multiple bookkeeping variables is that we have to change the signature of $alloca, malloc, or __SMACK_check_memory_safety procedures since they check/constrain/update different variables.
Motivation
Currently, we only have one bookkeeping variable
$Allocfor the entire program. We can split it into multiple bookkeep variables such that one variable roughly corresponds to one allocation site (i.e., a call tomallocor anallocainstruction). Having multiple bookkeeping variables reduces the solver's burden to reason about arrays.Implementation Plan
The key idea to implement this feature is to id allocation sites and find out which allocate sites a pointer is associated with.
However, an implication of having multiple bookkeeping variables is that we have to change the signature of
$alloca,malloc, or__SMACK_check_memory_safetyprocedures since they check/constrain/update different variables.