Several [invariant] at a program point
ID0000750: This issue was created automatically from Mantis Issue 750. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000750 | Frama-C | Kernel > ACSL implementation | public | 2011-03-08 | 2014-02-12 |
| Reporter | Anne | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
If we want to put several [invariant] annotations at a program point, we have to have several ACSL comment, else we get : [kernel] user error: Only one code annotation is allowed per comment But with several comments, several program points are created, and it is then difficult to interpret the invariants, because it seems that they have to be considered as a sequence, while we want to see them as a conjunction...
Would it be possible to have several invariants at the same point like it is done for le [loop invariant] ?
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information