[Bug] rflx generate aborts with a bug box #1309
Description
Executing rflx generate on https://github.com/mgrojo/coap_spark/blob/ff07007ae5182cb7a47ae7d901453f1e9b59aaaf/specs/coap_server.rflx raises the following bug box:
------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.25.0
attrs 23.2.0
defusedxml 0.7.1
pydantic 2.8.2
pydotplus 2.0.2
pygls 1.3.1
ruamel.yaml 0.18.6
setuptools 74.1.1
z3-solver 4.12.2.0
Optimized: False
Command: tools/RecordFlux//.venv/bin/rflx generate -d generated/ specs/coap_server.rflx
Traceback (most recent call last):
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/cli.py", line 459, in main
args.func(args)
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/cli.py", line 492, in generate
Generator(
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/generator.py", line 151, in generate
units = self._generate(model, integration)
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/generator.py", line 316, in _generate
units.update(self._create_state_machine(d, integration))
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/generator.py", line 341, in _create_state_machine
fsm_generator = FSMGenerator(
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 412, in __init__
self._create()
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 445, in _create
state_machine = self._create_state_machine()
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 645, in _create_state_machine
unit += self._create_states(self._state_machine, composite_globals, is_global)
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 1193, in _create_states
*[
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 1196, in <listcomp>
for s in self._state_action(
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 2951, in _state_action
result = self._assign(
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 3200, in _assign
return self._assign_to_call(target, expression, exception_handler, is_global, state)
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 4102, in _assign_to_call
self._to_ada_expr(self._convert_type(a, t), is_global),
File "/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/rflx/generator/state_machine.py", line 6455, in _convert_type
assert isinstance(target_type, (ty.Integer, ty.Enumeration)), target_type
AssertionError: message type "CoAP_Server::Definite_Message"
----------------------------------------------------------------------------
A bug was detected. Please report this issue on GitHub:
https://github.com/AdaCore/RecordFlux/issues/new?labels=bug
Include the complete content of the bug box shown above and all input files
in the report. Use plain ASCII or MIME attachment(s).
I attach the input files:
coap_spark_rflx.zip