Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002397Frama-CKernel > ACSL implementationpublic2018-08-27 18:122018-08-27 18:35
ReporterNewUser 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
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

- Relationships

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

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker