Track taint path

Is it possible to track in which execution paths (EG nodes) some tainted SVal or MemRegion is defined?
For example,

void foo() {
printf(“Here inBuf is not in the scope”);
// Tainted symbols:
// derived_$21{conj_$17{int, LC1, S33820, #1}, Element{SymRegion{conj_$14{void *, LC1, S33664,#1}},0 S64b, char}} : 0 (tag)
// checkDeadSymbols called when this foo under analysis messages that this tainted symbol isDead=0, i.e. live

int main() {

FILE *inFile = fopen(inFileName, “r”);

fread(inBuf, 1, inBufSize, inFile); // here inBuf becomes tainted


… // some other code, that used inBuf, so inBuf is live


Here I need to determine if inBuf cannot be obtained in foo() from the example programmer’s point of view.

Please, tell me is any decision exists?

If I understand correctly, there’s no readily available solution. You can use LocationContext to ask which function you’re in, but then you’ll need to scan the entire program state (Environment, Store, checker states) to confirm that the region hasn’t been passed in to your stack frame.

Usually we don’t need such machines though. Instead of proving that something can’t happen, we simply react when it does happen. Say, when somebody does something unsafe with a region, we can ask ourselves “hey, is it that region by any chance?” and emit a warning if so. Such direct questions are usually trivial to answer because we already know where to look.