--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on September 2013 ---
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?