I have installed the latest frama-c release (phosphorus) on Linux, and tried to define a global invariant, but got the message that is not supported yet by WP. What is the status about that ? Is there a documentation about what is supported in ACSL language ?
Thanks.
ACSL features supported by Frama-C's kernel are described in the ACSL implementation manual that is available for each release. For Phosphorus, it is here. If something is not supported by the kernel, it will of course not be supported by any plug-in either.
On the other hand, plug-ins tend to only support a given subset of what is available in the kernel. It is normally up to the plug-in documentation to precisely define this subset, but in the case of the WP manual, this seems to be missing. This probably ought to be considered as a bug.