How to add ACSL annotation for a new programme correctly and easily?
ID0000870: This issue was created automatically from Mantis Issue 870. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000870 | Frama-C | Kernel > ACSL implementation | public | 2011-06-24 | 2011-06-24 |
| Reporter | luoting | Assigned To | signoles | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
hello, I find it's difficult to add ACSL annotation for a programme .I have learned ACSL tutor material carefully. however ,I find it's still hard to add acsl for a new programme to specify its property.Would you please tell me which material should I study except for ACSL tutor materials in the frama-c.com . Thanks very much!