non-definite message in return type of function not allowed

[jklmnn]

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.

[senier]

@jklmnn Can you please add a reproducer to the issue description so we can easily check whether the problem persists?

[jklmnn]

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

[treiher]

Fixed by 49f8edf and 1ef5cc8.