[cfe-dev] Checking Model Used by 'ArrayBoundV2'

[Anna Zaks]

Benjamin,

The ArrayBoundV2 is based on symbolic execution analyses like most of the other analyzer checkers. There is no formal document which would help you easily identify false negatives/positives (source code and the analyzer site are the best sources of documentation). Currently, the main limitations are the lack of interprocedural analysis and a rather weak solver ( ex: it doesn't correctly model truncation). Feel free to file bugs for issues if you are unsure. Even if the analyzer doesn't reason about them now, they'd be valuable test cases to target as we make the analyses more powerful.

Cheers,
Anna.

On Dec 2, 2011, at 9:16 PM, Benjamin Schulz <bjs428 at mail.missouri.edu> wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
> 
> Hi all,
> 
> I was wondering if anyone could tell me what model of array bounds
> checking the static analyzer uses in
> '-analyzer-checker=experimental.security.ArrayBoundV2' ?  Is the
> implementation based on a checking algorithm or a type system that's
> been documented (formally or informally) elsewhere?
> 
> In particular, I'm trying to figure out which kinds of false negatives
> (e.g. http://llvm.org/bugs/show_bug.cgi?id=11114) should be viewed as
> bugs in the implementation, and which are necessary consequences of the
> checking procedure that's applied.
> 
> Thanks,
> 
> - --Benjamin Schulz
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.10 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
> 
> iQEcBAEBAgAGBQJO2bC+AAoJECT8Sbi31ptplJcIAM57sWzIXcOLp8KQxSMXKfpS
> coYWDN4fRxz+EcqXUgugs79fEepOto033aFOvZ3Oyt0PSs6IPExQAtNkWOro8Dcm
> tqGzJJydJW25WdtBQH911QhelJ5i26I4lj2Z0nl9FvSBjPkOqaU0phuAc3ATwbRx
> HiVajE1RGtlVJ553OLIvjymnZPFdlbYoHMhVw1nJ/iooMWGnGrrKjYnrZ1hxQ7O4
> ZLwc1LKJGzX/dGueubiqYo+WWE/rnWpw3xkG9U/oZ9IMQ9iY9zyadytjlv3vINcR
> kiJGGJYgSTnJoaXqxQ+WaJ5cMImlqko3u3/115cCkJSimlG0J3UVwCgqxFSlEXQ=
> =MMkC
> -----END PGP SIGNATURE-----
> 
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev