--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on September 2013 ---
> > In Frama-C libc headers, notation "((char*)ptr)[0..(nmemb*size)]" is used: > > /*@ assigns ((char*)ptr)[0..(nmemb*size)] \from *stream; */ > size_t fread(void * restrict ptr, > size_t size, size_t nmemb, > FILE * restrict stream); This nmemb*size should be nmemb*size-1. This is already fixed in Frama-C's development version. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130906/6031282e/attachment.html>