[cfe-dev] Path constraints at function call in checker

[Artem Dergachev via cfe-dev]

 > The desired information would be something
 > roughly analogous to { (x,  [2, 2147483647]),
 > (y,  [3, 2147483647]), (z, [4, 2147483647]) }.

The easiest way to *have a look* at these constraints is to dump() the 
program state and have them all printed out.

On the other hand, no matter how natural it is for the symbolic 
execution paradigm to be all about symbols and constraints, the analyzer 
doesn't provide a way to enumerate and act upon these constraints 
directly from, say, checker code.

The reason for this limitation is that the exact shape and contents of 
these constraints are defined by a replacable module - that implements 
the ConstraintManager interface - and different implementations of a 
ConstraintManager would store different information about symbols. The 
default implementation is called RangeConstraintManager. It can probably 
be replaced with a full-featured SAT solver, which would present the 
symbol range information in a completely different manner.

So if you want to obtain such information, then you probably have no 
choice but to add a pure-virtual method into ConstraintManager for 
obtaining all the info you need, and then implement it in 
RangeConstraintManager. Such method would be similar to print(). Ranges 
stored directly in RangeConstraintManager's program state trait are 
exactly what you need. If you're looking into printing the information 
to the user in a friendly manner, SValExplainer may come out handy for 
pretty-printing the symbols themselves.