The memory model (AKA heap abstraction) used by cclyzer++ relies on LLVM type information to create suballocations. This is inefficient - it can create too many suballocations, e.g., when creating array suballocations for indices that are never accessed. It is also unsound - it can create too few suballocations, e.g. in the examples in the documentation on unsoundness.
To solve these issues, we should migrate to a byte-offset based model of suballocations rather than a type-based one. These suballocations should be created on-demand as they are accessed by GEP instructions.
This is a research-level question, which will need a lot more design and discussion.
The memory model (AKA heap abstraction) used by cclyzer++ relies on LLVM type information to create suballocations. This is inefficient - it can create too many suballocations, e.g., when creating array suballocations for indices that are never accessed. It is also unsound - it can create too few suballocations, e.g. in the examples in the documentation on unsoundness.
To solve these issues, we should migrate to a byte-offset based model of suballocations rather than a type-based one. These suballocations should be created on-demand as they are accessed by GEP instructions.
This is a research-level question, which will need a lot more design and discussion.