Frama-C: Creating a ghost field in a non-ghost structure

My goal is to create a ghost field in a non-ghost structure. What I understand from the ACSL manual (v.1.17) is, that this is possible in ACSL:

If a structure has ghost fields, the sizeof of the structure is the same as the structure without ghost fields. Also, alignment of fields remains unchanged. (p. 82)

So my questions are:

1. How does a valid ACSL annotation look like to create a ghost field in a non-ghost structure?
2. Is it possible to programmatically create a ghost field as well?

I’m currently using Frama-C 25.0-beta (installed via opam).

Edit: added ACSL version

>Solution :

First of all, ghost fields in non-ghost structures are currently not supported by Frama-C, as mentioned in the ACSL implementation manual (https://www.frama-c.com/download/frama-c-acsl-implementation.pdf p84). So basically, it is impossible to write one that would be correctly handled by Frama-C and its plugins. Thus, about your second question, it is currently not possible and requires changes in both the Frama-C kernel and the plugins.

About your first question, if we follow the ACSL manual, it would something like this:

struct S {
  int f ;
};

/*@ ghost struct S {
  int g ;
};
*/

However, since (as far as I know) it is not implemented anywhere today, I think it could (and probably should) change when it will be implemented.