Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001939Frama-CKernel > libcpublic2014-10-19 21:092016-01-26 13:33
Reportermansour 
Assigned Tomaroneze 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0001939: Specification of the read function
DescriptionHi,

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
TagsNo tags attached.
Attached Filespatch file icon frama-c-Neon-20140301-read-spec.patch [^] (4,633 bytes) 2014-10-19 21:09 [Show Content]

- Relationships

-  Notes
(0005901)
maroneze (developer)
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 (http://stackoverflow.com/questions/28439055/ [^]) which you may find useful.
(0005902)
maroneze (developer)
2015-04-29 16:39

A few specifications will be present in the next release.

- Issue History
Date Modified Username Field Change
2014-10-19 21:09 mansour New Issue
2014-10-19 21:09 mansour Status new => assigned
2014-10-19 21:09 mansour Assigned To => virgile
2014-10-19 21:09 mansour File Added: frama-c-Neon-20140301-read-spec.patch
2015-04-29 14:15 maroneze Assigned To virgile => maroneze
2015-04-29 15:07 maroneze Note Added: 0005901
2015-04-29 16:39 maroneze Note Added: 0005902
2015-04-29 16:39 maroneze Status assigned => resolved
2015-04-29 16:39 maroneze Resolution open => fixed
2015-07-17 08:35 signoles Category Kernel > ACSL implementation => Kernel > libc
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker