2021-01-25 15:04 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002397Frama-CKernel > ACSL implementationpublic2018-08-27 18:35
Assigned Tovirgile 
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002397: Model Variables in Frama C
DescriptionThe 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?
TagsNo tags attached.
Attached Files




virgile (developer)

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.

-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