RecordFlux icon indicating copy to clipboard operation
RecordFlux copied to clipboard

crash with variable of private type

Open kanigsson opened this issue 4 years ago • 4 comments

The following session spec causes a crash of RecordFlux:

package Local_Id is
   type My_Int is mod 2 ** 8;

   generic
      type T is private;
      with function F return T;
   session Session with
      Initial => First,
      Final => Last
   is
      X : My_Int;
      Z : T;
   begin
     state First is
     begin
        X := 1;
        Z := F;
     transition
        then Last
     end First;

     state Last is null state;
   end Session;

end Local_Id;

Here is the bugbox:

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.0-pre
RecordFlux-parser 0.6.0
attrs 21.2.0
icontract 2.5.4
pydotplus 2.0.2
z3-solver 4.8.12.0

Optimized: True

Command: /home/kanig/dev/RecordFlux/venv/bin/rflx generate -d gen local_id.rflx

Traceback (most recent call last):
  File "/home/kanig/dev/RecordFlux/rflx/cli.py", line 120, in main
    args.func(args)
  File "/home/kanig/dev/RecordFlux/rflx/cli.py", line 176, in generate
    generator = Generator(
  File "/home/kanig/dev/RecordFlux/rflx/generator/generator.py", line 164, in __init__
    self.__generate(model)
  File "/home/kanig/dev/RecordFlux/rflx/generator/generator.py", line 239, in __generate
    self.__create_session(s)
  File "/home/kanig/dev/RecordFlux/rflx/generator/generator.py", line 242, in __create_session
    session_generator = SessionGenerator(session, self.__prefix, debug=self.__debug)
  File "/home/kanig/dev/RecordFlux/rflx/generator/session.py", line 146, in __init__
    self._create()
  File "/home/kanig/dev/RecordFlux/rflx/generator/session.py", line 180, in _create
    self._unit_part = self._create_state_machine()
  File "/home/kanig/dev/RecordFlux/rflx/generator/session.py", line 414, in _create_state_machine
    evaluated_declarations = self._evaluate_declarations(
  File "/home/kanig/dev/RecordFlux/rflx/generator/session.py", line 741, in _evaluate_declarations
    result += self._declare(
  File "/home/kanig/dev/RecordFlux/rflx/generator/session.py", line 882, in _declare
    fatal_fail(
  File "/home/kanig/dev/RecordFlux/rflx/error.py", line 199, in fatal_fail
    _fail(FatalError(), message, subsystem, severity, location)
  File "/home/kanig/dev/RecordFlux/rflx/error.py", line 210, in _fail
    error.propagate()
  File "/home/kanig/dev/RecordFlux/rflx/error.py", line 163, in propagate
    raise self
rflx.error.FatalError: local_id.rflx:12:7: generator: error: unexpected variable declaration for private type "T"

kanigsson avatar Aug 31 '21 03:08 kanigsson

Private types are not yet supported in the code generator. During the implementation of the session support, there were doubts about the necessity/usefulness of private types. We have to decide if we want to keep private types in the language.

treiher avatar Aug 31 '21 08:08 treiher

OK, thanks, feel free to kill this ticket.

kanigsson avatar Aug 31 '21 08:08 kanigsson

I would keep this ticket as a reminder to either implement private types in the generator or remove private types from the language.

treiher avatar Aug 31 '21 09:08 treiher

I created a new ticket (#1156) for the support (or removal) of private types.

senier avatar Aug 25 '22 09:08 senier

Obsoleted by #1156

senier avatar Nov 01 '22 14:11 senier