Skip to content

CrabMemoryDomains

Jorge Navas edited this page Mar 29, 2022 · 1 revision
  • 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.

Clone this wiki locally