static analysis: covers all possible control flows?

I'm thinking about writing a checker whose correctness depends on
analyzing all valid control flows through a given procedure's basic
blocks.

Does anyone know whether clang's static analyzer is guaranteed to
analyze a superset, subset, or the exact set of valid control flows?

Also, if there's an infinite loop within some procedure, how does the
static analyzer handle / present that?

Thanks,
Christian

Detecting infinite loops would be a classic "halting problem" (or its
inverse, specificially), which can not be solved by simple logic for
all cases. You may be able to detect SOME cases of infinite loops, but
certainly not all.

Hi Mats,

Thanks, I know that if clang static analyzer is guaranteed to
terminate, then it must allow some kind of imprecision in its results.
(I'm assuming it always terminates even if there's an infinite loop.)

I'm trying to understand what the imprecision looks like, from the
perspective of a checker, in the presence of loops and recursion.

I have a sense of how some static analysis algorithms handle this, but
I don't know much about how symbolic-evaluation-based analyzers do it.

I'm thinking about writing a checker whose correctness depends on
analyzing all valid control flows through a given procedure's basic
blocks.

Does anyone know whether clang's static analyzer is guaranteed to
analyze a superset, subset, or the exact set of valid control flows?

I am not 100% sure what you mean by valid control flows.

However, I think the answer is “neither". The analyzer tries to approximate the set of valid paths through the program. However, it may drop feasible paths (see the example with loops below). It also may cover an invalid path. For example, it may think that entering true branches of the two consecutive if statements is possible, when it is not:

if (cubed(y) == x) // The analyzer may not know that cubed(y) === y*y*y.
  a++;
if (y*y*y != x)
  a—;

Also, if there's an infinite loop within some procedure, how does the
static analyzer handle / present that?

The loops are “unrolled” a certain number of times. So given that the analyzer cannot precisely model the loop condition, you would get coverage for several path:
- the loop is not entered
- only one iteration of the loop is executed
- only two iterations of the loop are executed
- only three iterations of the loop are executed