[cfe-dev] checking function preconditions with Clang Static Analyser

[Anna Zaks]

On Jun 11, 2013, at 12:37 AM, Andrzej Krzemienski <akrzemi1 at gmail.com> wrote:

> Hi Everyone,
> I wonder if it would be possible to have Clang Static Analyser check if function's preconditions are satisfied before the call. A precondition is an expression, and static analyser would have to check if the same (or similar) expression has been explicitly checked by the programmer or is guaranteed by other function's postcondition.


Static analyzer would benefit form a programmer specifying pre- and postconditions in their code. Essentially, this is a way for the programmer to tell us more about their code, which makes it easier for us to find bugs. For example, we would check if a postcondition is violated after the function is executed and use the precondition to strengthen the set of assumptions on the function entry. Note that the analyzer will not be able to prove that the postcondition holds in general, we would just flag the cases where we can detect that it does not hold. (One could also insert runtime checks for these.)

Have you looked at Spec# research project, which includes a static program verifier? (http://research.microsoft.com/en-us/projects/specsharp/) 

SAL annotations are also somewhat related and those have been productized.

Anna.

> An example of what I mean is provided in the following post from group ISO C++ Standard - Future Proposals:
> https://groups.google.com/a/isocpp.org/d/msg/std-proposals/hUeCh-QCj0Y/aqX9W4ngjq0J
> 
> I am trying to determine if the addition of Contract Programming features to C++ is enough to enable such enhanced static analysis, or if it would be just a "dead" feature.
> 
> Regards,
> &rzej
> _______________________________________________
> 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/20130613/1d4cb288/attachment.html>