--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pointer comparable warnings and NULL test for parameter



Dear all,
When trying to analyse a function using value I get \pointer_comparable 
warnings for each test on pointer parameters (== NULL).
I did not manage to understand why it does so: the only clue I found is a 
post on the blog that considers more advanced situations than just 
comparing a pointer to NULL.
I have no particular background in program verification so may be the 
answer is obvious but I would like to know if it is possible to do 
something to remove those warnings. Below is a simple (and typical) 
example of program that lead to such warning.
#define NULL ((void*)0)

void f (int *tab)
{
  if ( tab != NULL )
  {
  // some functional code
  }
  else
  {
  // some error code
  }
}
Best Regards,
Beno?t GERARD

[ENVOYE PAR INTERNET] 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130320/1ad37ae8/attachment.html>