2

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

jobnz
  • 398
  • 3
  • 10
  • 1
    Minor remark: there is a difference between the [*ASCL specification*](https://github.com/acsl-language/acsl/releases/download/1.17/acsl.pdf) and its [implementation in Frama-C](https://www.frama-c.com/download/acsl-implementation-25.0-Manganese.pdf), just like there is a difference between, say, the [Java Language Specification](https://docs.oracle.com/javase/specs) and its [reference implementations](https://jdk.java.net/java-se-ri/18). Hence why, in theory, it's possible in *ACSL*, but not currently in *Frama-C*. – anol Aug 02 '22 at 06:37

1 Answers1

2

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.

Ksass'Peuk
  • 538
  • 2
  • 12