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
Assigned Tovirgile 
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 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
virgile (developer)
2018-08-27 18:35

The ACSL reference manual is indeed not entirely implemented by Frama-C. Each Frama-C release on contains a link to a manual giving the current support status of each ACSL feature. For Chlorine, this is 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 - 2020 MantisBT Team
Powered by Mantis Bugtracker