[cfe-dev] How does Static Analyzer handle ProgramStates?

[Jordan Rose]

Hi, Arthur. The analyzer does a couple things to keep from running out of memory. First, it uniques ProgramStates (and ExplodedNodes) that represent the same state reached along different paths. Second, each top-level function is analyzed separately, so even if you have a lot of functions in one file, the analyzer won't need to keep all paths for all functions in memory at once. Third, the analyzer limits the amount of possible nodes along a path in various ways: by bailing out of a loop after a few iterations, and by giving up on a path if it goes on too long. And fourth, if a particular analysis happens to be going on for long enough (measured by the number of nodes generated), the analyzer will give up on the function altogether.

These restrictions definitely restrict the power of the analyzer, and we've had many bugs filed about that, but we do want to make sure we don't tie up the user's whole computer. Furthermore, it's still an explicit goal for the analyzer that you should be able to analyze a small project in a reasonable amount of time, i.e. something that's not relegated to a nightly check.

As for your code, I'm wondering how it's valid at all (what type accepts an integer assignment and a pointer addition to that?), but please file a bug at http://llvm.org/bugs/ with a self-contained test case, because no matter how bad things are the analyzer still ought not to crash.

Jordan


On Jan 8, 2014, at 5:38 , Arthur Yoo <phjy007 at gmail.com> wrote:

> Hi all,
> 
> 
> 
> ProgramStates are immutable. Every ExplodedNode has its ProgramPoint and ProgramState. If the source code file is very very large, does the Analyzer can hold all of the PopgramStates for all paths?
> 
> 
> 
> In addition, I found it is strange when Analyzer evaluating ‘+=’ for some cases. My test codes are like below:
> 
> po = &obj;
> 
> a = 8;
> 
> a += po;
> 
> In my test, evaluating ‘a += po’ makes the Analyzer crash. However, if I try to evaluate the codes below, the Analyzer doesn’t crash.
> 
> po = &obj;
> 
> a = 8;
> 
> a = a + po;
> 
> So how can I solve this problem? Thanks a lot.
> 
> 
> -- 
> Best regards,
> Arthur Yoo
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20140108/d873e96b/attachment.html>