Split allocation tracking by SeaDsa class

[shaobo-he]

Fixes #768.

Summary

• derive allocation-liveness classes from SeaDsa alias classes
• pass the selected allocation map through stack, heap, global-allocation,
  free, and memory-safety-check helpers
• keep allocations unrelated to checked pointers in one fallback map
• preserve the reuse model's shared occupancy map for cross-class freshness

Design

Allocation classes are tracked separately from SMACK memory regions. A memory
region can represent a disjoint offset range within an object, but all offsets
of that object must observe the same allocation state. Consequently, a strict
one-to-one $Alloc.x to $M.x mapping would reject valid interior accesses.

The no-reuse models use the global monotonic address counter to keep allocation
classes disjoint, so their old shared $Alloc map can be removed. The reuse
model must still prevent simultaneously live allocations from different
classes from receiving overlapping addresses. It therefore keeps the existing
shared occupancy map for allocator freshness while dereference and free checks
use class-local liveness maps.

The allocator helpers take maps as values and return exact map updates. This
also replaces quantified frame conditions for the class-local state.

Evaluation

On a synthetic program with 32 independent allocation sites, end-to-end Boogie
times were:

memory model	shared map	allocation classes
no-reuse-impls	1.60-1.63 s	1.04-1.06 s
no-reuse	1.29-1.30 s	0.90-0.92 s
reuse	19.71-22.45 s	25.21-25.42 s

The reuse cost is expected from retaining global occupancy while adding local
liveness. The complete existing memory-safety suite remained approximately
neutral overall; the split pays off as the number of independent allocation
sites grows.

Testing

• 180/180 memory-safety configurations passed across no-reuse-impls,
  no-reuse, and reuse, using both Boogie and Corral
• all three memory models passed with --no-memory-splitting
• non-memory-safety malloc/free translation passed under all three models
• recursive clang-format check passed

Regressions cover independent allocation classes, classes merged through a
common pointer, and allocation/use/free across procedure boundaries.