Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] How would one annotate a function in an external header?
  • From: sstewartgallus00 at mylangara.bc.ca (Steven Stewart-Gallus)
  • Date: Fri, 06 Sep 2013 05:51:31 +0000 (GMT)
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?