ACSL set logic / frama-c syntax error

Question

I am using the Nitrogen version of Frama-c on Mac, and can't seem able to use the "set" logic, as documented in the ACSL manual, e.g., I can't declare a ghost variable as in "//@ ghost set<integer> someSet;".

The frama-c program always complains about a syntax error in the line where a set is declared, no matter what.

I also tried "Set" instead of "set", other types in place of "integer" (e.g. "char*")and specifying "//@ open set;" to import the module.

Maybe I need to specify some command line option? Executing "frama-c -kernel-help" it's not clear what that would be though.

Or maybe the Mac version (I downloaded the Intel binary version) is outdated and I should compile the latest source code ?

Thanks, best regards,

Eduardo

Answer 1

ACSL is an annotation language that exists independently of Frama-C, although some of the same persons work on both. From the point of view of usage of ACSL in a Frama-C plug-in, there are three levels of definition/implementation, and you need all three to be able to use a feature:

• The feature must be part of the ACSL language.
• It must be made available by the current Frama-C front-end. Not all features of the ACSL language are immediately implemented in the front-end.
• The plug-in you intend to use must take advantage of it.

Another explanation of the same distinction is here.

I can't declare a ghost variable as in "//@ ghost set someSet;".

In your case, it appears that the partially implemented feature is not so much sets (which seem implemented in the front-end after a quick look) but ghost code, which can currently only use C constructs and types.

Or maybe the Mac version (I downloaded the Intel binary version) is outdated and I should compile the latest source code ?

You have the latest version at this time.