AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
104 stars 6 forks source link

Support new versions of GNAT #1116

Closed jklmnn closed 2 years ago

jklmnn commented 2 years ago

Newer versions of GNAT require generic parameters to be marked as Ghost if they're ghost subprograms. If a ghost function is passed as a generic parameter, previously it had been done the same way as with a regular function:

generic
   with function Some_Ghost_Function return Boolean;
package Some_Package is

With newer GNAT versions such a parameter has to be explicitly marked as Ghost:

generic
   with function Some_Ghost_Function return Boolean with Ghost;
package Some_Package is

This behaviour is a problem in RecordFlux in the RFLX.RFLX_Message_Sequence package as the function Element_Initialized is usually ghost. Adding with Ghost would solve the problem but also breaks compatibility with older compilers. The fix here is to remove the Ghost aspect from the Initialized function of messages.