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

[Benjamin Schulz]

-----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-----