--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on August 2015 ---
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; } }