0002397: Model Variables in Frama C - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0002397

Frama-C

Kernel > ACSL implementation

public

2018-08-27 18:12

2018-08-27 18:35

Reporter

NewUser

Assigned To

virgile

Priority

normal

Severity

feature

Reproducibility

N/A

Status

assigned

Resolution

open

Platform

OS

OS Version

Product Version

Frama-C 17-Chlorine

Target Version

Fixed in Version

Summary

0002397: Model Variables in Frama C

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<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?

Tags

No tags attached.

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