[cfe-dev] adding assertion in C code and verifying using clang API

[Jordan Rose]

Clang does do a good job keeping track of source locations, and the SourceManager class can translate SourceLocations into line numbers. What you're actually trying to do is a bit harder, though.

If you just want to leverage the compiler for this, C11 already has this natively in the form of static_assert:

// clang -std=c11 main.c
#include <assert.h>

int main()
{
  int x = 10;
  static_assert(x > 0, "something is seriously wrong");
  return 0;
}

C++11 has the same thing, except you don't need to include <assert.h>.

If you want to do path-sensitive assertions, however, your job is much harder. A tool like the static analyzer has to assume it doesn't know everything, and so when it sees assert(a <= b), it takes that as a new fact. Now consider code like this:

int a = hasA ? 4 : 0;
int b = hasB ? 5 : 0;
assert(a <= b);

There are four possible cases here, but the assertion is false on one of them (hasA && !hasB). Should you get a warning there, or is it an "implicit assertion" that you will never have hasA without hasB? The static analyzer assumes the latter. Figuring out that you meant the former is difficult.

You could have another type of assertion that says "I think this should be statically provable along any path", and then have the analyzer warn when these assertions are violated, but I'm not sure adding yet another kind of assertion is a good idea for a codebase.

Anyway, that's the state of things. Sorry it's not a more encouraging answer!
Jordan


On May 13, 2013, at 4:50 , Rajendra <rks at cse.iitb.ac.in> wrote:

> I want to verify some user defined assertion in C code. e.g. 
> 
> int main()
> {
>  int x, y;
>  x = 10;
>  MYASSERT1: x>0; 
>  y = 0;
>  MYASSERT2: x==0; 
>  return 0;
> }
> 
> How does clang API (or any other tool) help to achieve this? besides I want
> to keep track of line number in original C code. 
> 
> All help is appreciated. 
> 
> 
> 
> --
> View this message in context: http://clang-developers.42468.n3.nabble.com/adding-assertion-in-C-code-and-verifying-using-clang-API-tp4032068.html
> Sent from the Clang Developers mailing list archive at Nabble.com.
> _______________________________________________
> 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/20130514/67e42238/attachment.html>