Flow-sensitive bounds declarations within expressions

[dtarditi]

We allow flow-sensitive bounds declarations for variables at the level of expression statements. However, expressions in C can themselves have control-flow, so we could allow flow-sensitive bounds declarations at the level of assignments within expressions. This would make sense for cases like e1, e2, e3 or e1 ? e2 : e3.

We would need to describe how flow-sensitively determine bounds declarations. We could follow the same pattern used in checking of bounds declarations for analyzing expressions, except gather bounds declarations instead.