[cfe-dev] [analyzer] Random SVal hierarchy questions.

[Devin Coughlin via cfe-dev]

> On Nov 17, 2015, at 7:53 AM, Artem Dergachev via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Hmm, i think i can answer myself regarding conjured structures, after a bit of thinking. There's really nothing wrong with symbols of structural type - in fact, it has been some kind of a dream for me to consider complicated constraints on structures, and especially on containers - consider a solver that can handle constraints like "this symbolic set is a subset of that symbolic set", or SymSymExpr's like "this set is an intersection of these two sets", etc., which can be achieved with structure-type symbols. Probably even strings would be modeled better with string-symbols and constraints than with stores. So i think it's all right to keep the current situation, even though we're not quite using these capabilities yet, and i withdraw this idea.

Yes, any operation on structs you could view as an uninterpreted function could be represented in this way quite simply, although more complicated theories would be challenging to reason about without deferring to a dedicated solver such as Z3 or CVC4.

Devin