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

[Jonathan Foote via cfe-dev]

Hello,

Is there a simple way to enumerate all of the constrained symbolic values (and constraints) required to reach a function call (where the call is outside the current translation unit) via symbolic execution in a Clang checker? For example, I'd like to get information about x, y and z at in this case:

```
int x = read();
int y = read();
int z = read();
if (x > 1 && y > 2 && z > 3) {
  foo(x);
}
```

The desired information would be something roughly analogous to { (x,  [2, 2147483647]), (y,  [3, 2147483647]), (z, [4, 2147483647]) }. I've tried a few different methods to elicit this information in the PreCall and PostCall hooks, but it seems that the ConstraintManager only is tracking constraints on the arguments to `foo`. 

I've reviewed the available documentation and re-watched the "Building a Checker in 24 Hours" talk (which was great BTW). I've also taken a look at some of the existing checkers to see how I might inform the execution to track constraints on these values, but nothing is jumping out at me.

I know there are some advertised limitations on symbolic execution in the checker framework but it seems like this should be possible. I'm new to clang internals so pardon if I missed something obvious.

Thanks,
Jon