| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0000750 | Frama-C | Kernel > ACSL implementation | public | 2011-03-08 17:27 | 2014-02-12 16:54 | ||||||||
| Reporter | Anne | ||||||||||||
| Assigned To | virgile | ||||||||||||
| Priority | normal | Severity | feature | Reproducibility | always | ||||||||
| Status | acknowledged | Resolution | open | ||||||||||
| Product Version | |||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0000750: Several [invariant] at a program point | ||||||||||||
| 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] ? | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
virgile (developer) 2011-03-08 18:35 |
This seems reasonable, but requires a change in ACSL specification itself before modifying the implementation. |
|
patrick (developer) 2011-03-11 08:38 |
In fact, plug-ins can generate several code annotations related to a unique statement. The kind of these code annotations may be different. An order as been defined between these kinds at the pretty printing: asserts < stmt contract < invariants < pragmas < loop annotations but it wasn't used until next commit. |
|
patrick (developer) 2011-03-11 08:47 |
Anyway, something seems to be needed at the ACSL level to ensure re-entrance. Today, pretty printing a C project having several code annotations at the same points, and parsing that output doesn't produce the same links between stmts and code annotations. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-03-08 17:27 | Anne | New Issue | |
| 2011-03-08 17:27 | Anne | Status | new => assigned |
| 2011-03-08 17:27 | Anne | Assigned To | => virgile |
| 2011-03-08 18:35 | virgile | Note Added: 0001570 | |
| 2011-03-08 18:35 | virgile | Status | assigned => acknowledged |
| 2011-03-11 08:38 | patrick | Note Added: 0001588 | |
| 2011-03-11 08:40 | svn | ||
| 2011-03-11 08:47 | patrick | Note Added: 0001590 | |
| 2013-12-19 01:12 | patrick | Source_changeset_attached | => framac master 71d60a65 |
| 2014-02-12 16:54 | patrick | Source_changeset_attached | => framac stable/neon 71d60a65 |
| Issue History |