AdaCore / RecordFlux

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

C code generator #1286

Open jklmnn opened 1 year ago

jklmnn commented 1 year ago

While the generated SPARK code is already architecture independent there are still platforms that don't have an Ada compiler at all. To increase the portability of RecordFlux a C code generator can be added.

The C code generator would consist of two major parts:

Additionally the rflx executable needs to be adapted to allow the selection of the desired output language. For that I propose the following parameter:

--target-language=<language>

The default value for the language would be spark. This pattern allows to introduce further languages in the future without needing to add new parameters.