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

Invalid "always true" error for enum with `Always_Valid` aspect #1276

Closed treiher closed 1 year ago

treiher commented 1 year ago
package Test is

   type T is (E) with Size => 16, Always_Valid;

   type M is
      message
         A : T;
         B : T
           if A = E;
      end message;

end Test;
tmp/test.rflx:8:10: model: error: condition "A = Test::E" on transition "B" -> "Final" is always true

The error message is wrong in this case, as A can have other valid values than the value represented by the literal E.

treiher commented 1 year ago

Fixed in version 0.12.0.