Model Variables in Frama C
ID0002397: This issue was created automatically from Mantis Issue 2397. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002397 | Frama-C | Kernel > ACSL implementation | public | 2018-08-27 | 2018-08-27 |
| Reporter | NewUser | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 17-Chlorine | Target Version | - | Fixed in Version | - |
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 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?
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information