--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] fopen and null pointers



Hello,

Le 18/08/2015 06:11, Tim Newsham a écrit :
>    fp = fopen("./seq","r");
>    /*@ assert Value: ptr_comparison: \pointer_comparable(fp, (void *)0); */
>
> Is there a way I can annotate this call or the fopen function
> to specify that NULL is a valid return value?


Use the standard headers (see attached example).

But in your example (at least in mine), the warning is coming from 
garbled mix in "fp" (comparison with a variable containing garbled mix). 
I don't know *why* this garbled mix occurs though.

   frama-c -val tim-fopen.c
[...]
[value] Values at end of function main:
   fp ∈
     {‌{ garbled mix of &{__fc_fopen; alloced_return_fopen}
      (origin: Arithmetic {tim-fopen.c:8}) }‌}


Best regards,
david

-------------- next part --------------
#include <stdio.h>
#include <stdlib.h>

int main(void)
{
  FILE *fp;

  fp = fopen("./seq","r");
  if (fp == NULL) {
    return 0;
  } else {
    return 1;
  }
}