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

[Frama-c-discuss] How would one annotate a function in an external header?



I'm interested in exploring Frama-C in an unusual manner which is by creating a
tiny toy 3D game application. I plan on making this feasible by dividing my
application up into several isolated processes that communicate through message
passing. All my unverified code which will struggle against large, ugly, and
unsafe APIs like OpenGL, or SDL will be contained inside separate processes
(sort of like Google's Chromium.) There is currently, an ongoing attempt to
formalise, and provide annotations for the standard libraries APIs but
unfortunately not that much has been done yet. For that reason, I wish to write
some of my own annotations such as the following (probable incorrect [I'm still
pretty new at using frama-c]) one for the fread function which is is supposed to
declare that the fread function initializes the data it reads into.

/*@
  ensures ? integer ii;
  ii >= 0 ? ii < \result * size ? \initialized(&((char *)ptr)[ii]);
*/
extern size_t fread(void *ptr, size_t size, size_t nmemb, FILE *stream);

How would one attach an annotation to a function declared in an external header?