View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001939 | Frama-C | Kernel > libc | public | 2014-10-19 21:09 | 2016-01-26 13:33 | ||||
Reporter | mansour | ||||||||
Assigned To | maroneze | ||||||||
Priority | normal | Severity | feature | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Neon-20140301 | ||||||||
Target Version | Fixed in Version | Frama-C Magnesium | |||||||
Summary | 0001939: Specification of the read function | ||||||||
Description | 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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
maroneze (administrator) 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. |
maroneze (administrator) 2015-04-29 16:39 |
A few specifications will be present in the next release. |
![]() |
|||
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 |