Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Pointer comparable warnings and NULL test for parameter
  • From: benoit.gerard at dga.defense.gouv.fr (benoit.gerard at dga.defense.gouv.fr)
  • Date: Wed, 20 Mar 2013 09:49:06 +0100
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>