Resending finished email (grr... at email client). ----- Taras Glek <[email protected]> wrote: > The two errors I looked at, seem to be false positives
Hi, yeah, the great majority of these reports are going to be false positives (I hope that was clear from the talk!). The trick here is that it should be clear from the report where the tool got confused, and it should be easy to add an annotation which the tool can use to check the assertion. For both of these reports, the tool picked the wrong postcondition for a called function, and in both the right postcondition is easy to specify. > http://sixgill.org/firefox/write_overflow/ResolveSymlink_1244447419593944471.html The first step the tool took for this access was pick the (wrong) postcondition (__return < 4097) for PR_Read: PR_IMPLEMENT(PRInt32) PR_Read(PRFileDesc *fd, void *buf, PRInt32 amount); Adding __postcondition(return <= amount) will fix this report (the same postcondition would have to be added to pl_DefRead due to its potential recursion, this is an issue with the tool that needs to be fixed). > http://sixgill.org/firefox/write_overflow/EncodeString_3315072988729628109.html > Again, the first step the tool took was picking a wrong postcondition for nsEncoderSupport::Convert. nsresult nsEncoderSupport::Convert(const PRUnichar * aSrc, PRInt32 * aSrcLength, char * aDest, PRInt32 * aDestLength) This can be fixed with a precondition and postcondition describing this interface: __precondition(ubound(aDest) >= *aDestLength) __postcondition(ubound(aDest) >= *aDestLength) (An alternative would be __postcondition(*aDestLength <= initial(*aDestLength)) where initial indicates the value at function entry for a term. This isn't supported yet though (would be easy to fix)). Doing this is more work than using a bugfinder, a tool that guesses which accesses are likely to be bugs. Once the code is annotated though, you get strong guarantees (not airtight yet) that *all* the bugs have been found; with a bugfinder you don't get anything. Also, improvements to the tool's inference will reduce the need for annotations. In both the above cases it would not be too hard to work on the tool to infer these and similar postconditions. Brian _______________________________________________ dev-static-analysis mailing list [email protected] https://lists.mozilla.org/listinfo/dev-static-analysis
