Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
treiher opened this issue Dec 21, 2022 · 1 comment
Closed

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

treiher opened this issue Dec 21, 2022 · 1 comment
Assignees
Labels
bug model Related to model package (e.g., model verification)

Comments

@treiher
Copy link
Collaborator

treiher commented Dec 21, 2022

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 treiher added bug model Related to model package (e.g., model verification) labels Dec 21, 2022
@treiher treiher added this to Medium in RecordFlux Future via automation Dec 21, 2022
@treiher treiher self-assigned this Aug 21, 2023
@treiher
Copy link
Collaborator Author

treiher commented Aug 21, 2023

Fixed in version 0.12.0.

@treiher treiher closed this as completed Aug 21, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug model Related to model package (e.g., model verification)
Projects
No open projects
Development

No branches or pull requests

1 participant