Specification of the read function
ID0001939: This issue was created automatically from Mantis Issue 1939. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001939 | Frama-C | Kernel > libc | public | 2014-10-19 | 2016-01-26 |
| Reporter | mansour | Assigned To | maroneze | Resolution | fixed |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | Frama-C Magnesium |
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