Search code examples
frama-c

Model variables in Frama-C

Model variables are described in the Frama-C manual (both in the spec and the "implementation" version).

However I am unable to parse a simple fragment such as the one in the manual, eg.

//@ model set<integer > forbidden = \empty;

or even

//@ model integer x = 0;

lead to parse errors.

Are model variables really supported? If so, what am I doing wrong? The version of frama-c I'm using is Nitrogen on MacOS.

Thanks, Eduardo

Solution

  • As mentioned p.11 of the "implementation" version of the ACSL manual, the features written in a red font are not yet available in Frama-C. Indeed in Nitrogen, neither model variables nor model fields are implemented.