Avoid unnecessary global allocations in memory-safety checks

[shaobo-he]

Summary

• use SeaDsa's propagated read/modified flags to identify globals involved in memory accesses
• omit $galloc calls for globals proven unrelated to those accesses
• retain allocations for accessed globals, including accesses reached through aliases

Rationale

Every $galloc call introduces quantified allocation constraints. Globals that are only passed to an external declaration, such as the string in the issue reproduction, do not need those constraints. SeaDsa's node flags provide a conservative interprocedural criterion: aliases share and propagate the read/modified state.

Testing

• built and installed SMACK with LLVM 14
• passed all 174 memory-safety combinations: 29 tests, three memory models, and Corral/Boogie
• passed the repository-wide clang-format check
• added regressions for the exact unused-string reproduction and alias-mediated global access

Fixes #716