Frama-C Bug Tracking System - Frama-C
View Issue Details
0001939Frama-CKernel > libcpublic2014-10-19 21:092016-01-26 13:33
Frama-C Neon-20140301 
Frama-C Magnesium 
0001939: Specification of the read function
Hi, I think it would be useful to have a specification of common libc functions included with Frama-C (instead of repeating them in many projects), so I started with one for the read function. I think it's complete, but I am still new to ACSL, so correct me if I'm wrong. Please find attached the diff to the Neon version. Yours, Mansour
No tags attached.
patch frama-c-Neon-20140301-read-spec.patch (4,633) 2014-10-19 21:09
Issue History
2014-10-19 21:09mansourNew Issue
2014-10-19 21:09mansourStatusnew => assigned
2014-10-19 21:09mansourAssigned To => virgile
2014-10-19 21:09mansourFile Added: frama-c-Neon-20140301-read-spec.patch
2015-04-29 14:15maronezeAssigned Tovirgile => maroneze
2015-04-29 15:07maronezeNote Added: 0005901
2015-04-29 16:39maronezeNote Added: 0005902
2015-04-29 16:39maronezeStatusassigned => resolved
2015-04-29 16:39maronezeResolutionopen => fixed
2015-07-17 08:35signolesCategoryKernel > ACSL implementation => Kernel > libc
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed

2015-04-29 15:07   
Thank you for the suggestions. One of the issues in specifying (at least part of) the libc is that there's no consensus about the level of detail that would be useful/necessary for some people, and that would not be excessive for others. For instance, several functions in the libc are stateful and would benefit from the introduction of model/ghost variables, but introducing too many of these imposes a burden on users who do not require such precision. Still, it is likely that a few functions, such as read, will have a default specification in the next release of Frama-C. In the meanwhile, there is a question related to read on Stack Overflow ( which you may find useful.
2015-04-29 16:39   
A few specifications will be present in the next release.