adding assertion in C code and verifying using clang API

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

adding assertion in C code and verifying using clang API

Rajendra
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.
Reply | Threaded
Open this post in threaded view
|

Re: adding assertion in C code and verifying using clang API

Rajendra
Has anyone on this forum explored this to check assertion? If so, please reply.
Reply | Threaded
Open this post in threaded view
|

Re: adding assertion in C code and verifying using clang API

Jordan Rose
In reply to this post by Rajendra
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 <[hidden email]> 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
[hidden email]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev