| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0002397 | Frama-C | Kernel > ACSL implementation | public | 2018-08-27 18:12 | 2018-08-27 18:35 | ||||||||
| Reporter | NewUser | ||||||||||||
| Assigned To | virgile | ||||||||||||
| Priority | normal | Severity | feature | Reproducibility | N/A | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Product Version | Frama-C 17-Chlorine | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0002397: Model Variables in Frama C | ||||||||||||
| Description | The model variables in FramaC are giving errors whenever I tried to use them in specification e.g the following code in ACSL manual complaints at line 3 (unexpected token 'forbidden'): /* public interface */ //@ model set<integer> forbidden = \empty; /*@ assigns forbidden; ensures ! ( \result \in \old(forbidden)) && \result \in forbidden && \subset(\old(forbidden),forbidden); */ int gen(); p.s: please share if any further examples of model variables available in FramaC? | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
virgile (developer) 2018-08-27 18:35 |
The ACSL reference manual is indeed not entirely implemented by Frama-C. Each Frama-C release on http://frama-c.com/download.html contains a link to a manual giving the current support status of each ACSL feature. For Chlorine, this is http://frama-c.com/download/acsl-implementation-Chlorine-20180501.pdf and it is indeed stated in section 2.11.2 that only model fields are supported (more precisely, unsupported features, such as model variables, are indicated in red in this document). The longer term goal is of course to support the whole ACSL language, but there is currently no precise timeline for model variables. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2018-08-27 18:12 | NewUser | New Issue | |
| 2018-08-27 18:12 | NewUser | Status | new => assigned |
| 2018-08-27 18:12 | NewUser | Assigned To | => virgile |
| 2018-08-27 18:35 | virgile | Note Added: 0006637 | |
| 2018-08-27 18:35 | virgile | Priority | urgent => normal |
| 2018-08-27 18:35 | virgile | Severity | minor => feature |
| Issue History |