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) in a Clang checker? For example, foo 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 but it seems like this should be possible. I’m new to clang internals so pardon if I missed something obvious.
Thanks,
Jon