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

Ping example is not proven #1256

Closed treiher closed 1 year ago

treiher commented 1 year ago

The currently used SPARK version has a bug which leads to an exit code 0 even in case of warnings and the use of --warnings=error (V819-006). We should fix the warnings and switch to a more recent SPARK version (>= 2022-08-22).