I'm looking forward to implement various checkers for detecting strange conditions which may be simplified or probably contain logical errors / typos. As for now it looks like CSA is missing some sort of single pass symbolic execution feature which would allow us to:
1. Simplify path sensitive symbolic execution and modeling by pre-computing and clarification constraints.
2. Quite cheap (as it will be single path) detection mechanism for various errors in complicated (or not) expressions by applying such constrains to the parts of condition (or whole condition) and so on.
3. Probably can be used in other tools such as clang-tidy, e.g. various recommendations how some expr can be simplified.
On the other hand, I'm rookie one to CSA and not quite familiar with core architecture but for me it looks like that would require modification of core analyzer engine and it's not easy task.