CrabMemoryDomains

Some slides here describing a simple allocation-site abstraction for memory regions with support for dynamic memory allocation. The domain is called region domain. Recency-like abstractions are not currently available but they will be soon.

Crab also provides array abstract domains. Currently, Crab provides the two extremes: an array smashing domain that represents all array elements into a single summarized element, and an expansion array domain that represents each individual array element with a ghost numerical variable. The latter can be optionally smashed if the number of elements reaches a threshold. Due to this behavior, it is called the array adaptive domain.