Frama-C Bug Tracking System - Frama-C
View Issue Details
0002397Frama-CKernel > ACSL implementationpublic2018-08-27 18:122018-08-27 18:35
NewUser 
virgile 
normalfeatureN/A
assignedopen 
Frama-C 17-Chlorine 
 
0002397: Model Variables in Frama C
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?
No tags attached.
Issue History
2018-08-27 18:12NewUserNew Issue
2018-08-27 18:12NewUserStatusnew => assigned
2018-08-27 18:12NewUserAssigned To => virgile
2018-08-27 18:35virgileNote Added: 0006637
2018-08-27 18:35virgilePriorityurgent => normal
2018-08-27 18:35virgileSeverityminor => feature

Notes
(0006637)
virgile   
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.