[cfe-dev] static analysis: covers all possible control flows?

[Christian Convey]

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.

On Tue, Jan 6, 2015 at 12:53 PM, mats petersson <mats at planetcatfish.com> wrote:
> 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.
>
> --
> Mats
>
> On 6 January 2015 at 15:24, Christian Convey <christian.convey at gmail.com> wrote:
>> 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
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev