[cfe-dev] Handling of loops in the Clang Static Analyzer

[Daniel Marjamäki via cfe-dev]

Hello!

> I did not quite realize it earlier but it seems that the static analyzer unrolls a loop up to a certain number of times and then stops exploring paths beyond that.

Yes that is how it is working. It is not perfect.

> I understand that handling loops is a difficult problem, but is there a work-around available, perhaps, even some source annotation from the user?

Perhaps there are work-arounds, I know that people have looked at this.

Maybe -analyzer-max-loop is interesting. It tells Clang analyzer how many times you want to go through loops. The bigger value the better analysis, but slower analysis.

    clang -cc1 -analyze -analyzer-checker=alpha,core -analyzer-max-loop 10000 test1.c

Best regards,
Daniel Marjamäki

..................................................................................................................
Daniel Marjamäki Senior Engineer
Evidente ES East AB  Warfvinges väg 34  SE-112 51 Stockholm  Sweden

Mobile:                 +46 (0)709 12 42 62
E-mail:                 Daniel.Marjamaki<mailto:Daniel.Marjamaki at evidente.se>@evidente.se<mailto:Daniel.Marjamaki at evidente.se>

www.evidente.se
________________________________
From: cfe-dev [cfe-dev-bounces at lists.llvm.org] on behalf of Venugopal Raghavan via cfe-dev [cfe-dev at lists.llvm.org]
Sent: 24 February 2017 04:07
To: cfe-dev at lists.llvm.org
Subject: [cfe-dev] Handling of loops in the Clang Static Analyzer

Hi,

I am re-sending the question I asked under a different thread so that the subject is more relevant to the topic.

I did not quite realize it earlier but it seems that the static analyzer unrolls a loop up to a certain number of times and then stops exploring paths beyond that. In the checker I have written, I get the message "Block count exceeded" and then state exploration stops. As a result, my checker give false positives and does not achieve what it sets out to do.

I understand that handling loops is a difficult problem, but is there a work-around available, perhaps, even some source annotation from the user?

Also, would it not be possible to re-start exploration after the loop if there is some code independent of the loop computation. I understand that this independent flow would eventually merge with the computation in the loop in some manner (otherwise the loop computation would probably have been "dead"), but, even then, it may be possible to so some useful analysis with the "independent" code.

Finally, I understand that the checkers have been used with "realistic" test cases. I am curious, how did they work if the test cases had loops in them?

Thanks.

Regards,
Venugopal Raghavan.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170224/108a4411/attachment.html>