RecordFlux
RecordFlux copied to clipboard
Published
20 hours ago •
AdaCore
AdaCore
non-definite message in return type of function not allowed
I'm getting the following error when trying to return a non-defined message in a function:
------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.0-pre
RecordFlux-parser 0.10.0
ruamel.yaml 0.17.21
pydantic 1.9.0
icontract 2.6.1
attrs 21.4.0
pydotplus 2.0.2
z3-solver 4.8.15.0
Optimized: False
Command: /tmp/tmp.SsozY8IYr3/venv/bin/rflx --no-verification generate specs/spdm.rflx specs/spdm_responder.rflx specs/spdm_emu.rflx specs/spdm_proxy.rflx --debug -d build/debug/generated
Traceback (most recent call last):
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/cli.py", line 201, in main
args.func(args)
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/cli.py", line 259, in generate
generator = Generator(
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 175, in __init__
self.__generate(model, integration)
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 250, in __generate
self.__create_session(s, integration)
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/generator.py", line 261, in __create_session
session_generator = SessionGenerator(
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 219, in __init__
self._create()
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 249, in _create
state_machine = self._create_state_machine()
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 353, in _create_state_machine
unit += self._create_abstract_functions(self._session.parameters.values())
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 515, in _create_abstract_functions
result.extend(self._create_abstract_function(parameter))
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/generator/session.py", line 556, in _create_abstract_function
fatal_fail(
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/error.py", line 200, in fatal_fail
_fail(FatalError(), message, subsystem, severity, location)
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/error.py", line 211, in _fail
error.propagate()
File "/tmp/tmp.SsozY8IYr3/venv/lib/python3.9/site-packages/rflx/error.py", line 164, in propagate
raise self
rflx.error.FatalError: specs/spdm_responder.rflx:124:7: generator: error: non-definite message in return type of function "Plat_Get_Meas_Signature" not allowed
----------------------------------------------------------------------------
I see why this is not supported (yet) but we may want to print an error message in when checking the spec instead of ending up in a bug box.
@jklmnn Can you please add a reproducer to the issue description so we can easily check whether the problem persists?
This spec reproduces the problem:
package Test is
type Message is
message
Data : Opaque;
end message;
generic
Channel : Channel with Writable;
with function Get_Message return Message;
session Session with
Initial => Start,
Final => Terminated
is
Global_Msg : Message;
begin
state Start
is
begin
Global_Msg := Get_Message;
transition
goto Send
end Start;
state Send
is
begin
Channel'Write (Global_Msg);
transition
goto Terminated
end Send;
state Terminated is null state;
end Session;
end Test;
It checks fine:
rflx check test.rflx
Parsing test.rflx
Processing Test
but produces the following error on generate:
rflx generate test.rflx -d out
Parsing test.rflx
Processing Test
Generating Test::Message
Generating Test::Session
------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.1.dev6+g69d65226
RecordFlux-parser 0.11.0
attrs 21.4.0
icontract 2.6.2
pydantic 1.9.2
pydotplus 2.0.2
ruamel.yaml 0.17.21
z3-solver 4.10.2.0
Optimized: True
Command: rflx generate test.rflx -d out
Traceback (most recent call last):
File "/.../RecordFlux/rflx/cli.py", line 215, in main
args.func(args)
File "/.../RecordFlux/rflx/cli.py", line 273, in generate
Generator(
File "/.../RecordFlux/rflx/generator/generator.py", line 142, in generate
units = self._generate(model, integration)
File "/.../RecordFlux/rflx/generator/generator.py", line 265, in _generate
units.update(self._create_session(s, integration))
File "/.../RecordFlux/rflx/generator/generator.py", line 282, in _create_session
session_generator = SessionGenerator(
File "/.../RecordFlux/rflx/generator/session.py", line 188, in __init__
self._create()
File "/.../RecordFlux/rflx/generator/session.py", line 218, in _create
state_machine = self._create_state_machine()
File "/.../RecordFlux/rflx/generator/session.py", line 334, in _create_state_machine
unit += self._create_abstract_functions(self._session.parameters.values())
File "/.../RecordFlux/rflx/generator/session.py", line 497, in _create_abstract_functions
result.extend(self._create_abstract_function(parameter))
File "/.../RecordFlux/rflx/generator/session.py", line 538, in _create_abstract_function
fatal_fail(
File "/.../RecordFlux/rflx/error.py", line 198, in fatal_fail
_fail(FatalError(), message, subsystem, severity, location)
File "/.../RecordFlux/rflx/error.py", line 209, in _fail
error.propagate()
File "/.../RecordFlux/rflx/error.py", line 162, in propagate
raise self
rflx.error.FatalError: test.rflx:10:7: generator: error: non-definite message in return type of function "Get_Message" not allowed