Bug when comparing opaque values

[NickFoubert]

I've been trying to figure out how to compare opaque values, and while trying out one iteration I've bumped into a bug.

Reproducer:

package Bug is

   type Message is
      message
         Key : Opaque with Size => 3 * 8;
      end message;

   type Messages is sequence of Message;

   generic
   session Session is
   begin
      state S is
        Ms_1     : Messages;
        Ms_2     : Messages;
        Test_Key : Opaque := [0, 1, 0];
      begin
        Ms_1'Reset;
        Ms_2'Reset;
        Ms_2 :=
            [for M in Ms_1
             if M.Key = Test_Key =>
             M];
      transition
         goto null
      exception
         goto null
      end S;

   end Session;
end Bug;

generating results in the following output:

Parsing specs/bug.rflx
Processing Bug
Verifying __BUILTINS__::Boolean
Verifying __INTERNAL__::Opaque
Verifying Bug::Message
Verifying Bug::Messages
Verifying Bug::Session
Generating Bug::Message
Generating Bug::Messages
Generating Bug::Session

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.15.0
attrs 23.1.0
icontract 2.6.5
importlib-resources 6.1.1
pydantic 1.10.13
pydotplus 2.0.2
pygls 1.0.2
ruamel.yaml 0.17.40
z3-solver 4.12.2.0

Optimized: False

Command: /usr/local/bin/rflx --workers 20 generate -d generated/ specs/bug.rflx

Traceback (most recent call last):
  File "/usr/local/lib/python3.11/dist-packages/rflx/cli.py", line 413, in main
    args.func(args)
  File "/usr/local/lib/python3.11/dist-packages/rflx/cli.py", line 507, in generate
    ).generate(
      ^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/generator.py", line 143, in generate
    units = self._generate(model, integration)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/generator.py", line 322, in _generate
    units.update(self._create_session(s, integration))
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/generator.py", line 339, in _create_session
    session_generator = SessionGenerator(
                        ^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 181, in __init__
    self._create()
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 214, in _create
    state_machine = self._create_state_machine()
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 379, in _create_state_machine
    unit += self._create_states(self._session, composite_globals, is_global)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/session.py", line 843, in _create_states
    Variable("Ctx.P.Slots" * self._allocator.get_slot_ptr(d.location)),
                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.11/dist-packages/rflx/generator/allocator.py", line 121, in get_slot_ptr
    slot_id: int = self._allocation_slots[location]
                   ~~~~~~~~~~~~~~~~~~~~~~^^^^^^^^^^
KeyError: 
    Location(
        _source=PosixPath('specs/bug.rflx'),
        _start=(22, 17),
        _end=(22, 22),
        _verbose=False)

----------------------------------------------------------------------------

A bug was detected. Please report this issue on GitHub:

[treiher]

Thank you for your report! We will look into it and get back to you.

[treiher]

We fixed the fatal error. Unfortunately, comparing opaque message fields requires some additional work and is not yet supported. For now, an error message will be displayed in this case.