Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Empty opaque value in function call detected as list comprehension #1146

Open
jklmnn opened this issue Aug 19, 2022 · 0 comments
Open

Empty opaque value in function call detected as list comprehension #1146

jklmnn opened this issue Aug 19, 2022 · 0 comments
Labels
bug specification Related to specification package (e.g., specification parsing)

Comments

@jklmnn
Copy link
Member

jklmnn commented Aug 19, 2022

Trying to call a function with an empty opaque value as follows:

with function Platform_Function (Data : Opaque) return Result_Type;
...
Result := Platform_Function ([]);

causes the following error:

Traceback (most recent call last):
  File "/.../RecordFlux/tests/integration/feature_test.py", line 112, in test_executability
    assert assert_executable_code(model, integration, tmp_path, main=MAIN) == config.sequence
  File "/.../RecordFlux/tests/utils.py", line 171, in assert_executable_code
    assert_compilable_code(
  File "/.../RecordFlux/tests/utils.py", line 149, in assert_compilable_code
    _create_files(tmp_path, model, integration, main, prefix, debug)
  File "/.../RecordFlux/tests/utils.py", line 271, in _create_files
    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 338, in _create_state_machine
    unit += self._create_states(self._session, composite_globals, is_global)
  File "/.../RecordFlux/rflx/generator/session.py", line 834, in _create_states
    *[
  File "/.../RecordFlux/rflx/generator/session.py", line 837, in <listcomp>
    for s in self._state_action(
  File "/.../RecordFlux/rflx/generator/session.py", line 1923, in _state_action
    result = self._assign(
  File "/.../RecordFlux/rflx/generator/session.py", line 2212, in _assign
    return self._assign_to_call(target, expression, exception_handler, is_global, state)
  File "/.../RecordFlux/rflx/generator/session.py", line 3236, in _assign_to_call
    *[a.substituted(self._substitution(is_global)).ada_expr() for a in arguments],
  File "/.../RecordFlux/rflx/generator/session.py", line 3236, in <listcomp>
    *[a.substituted(self._substitution(is_global)).ada_expr() for a in arguments],
  File "/.../RecordFlux/venv/lib/python3.9/site-packages/icontract/_checkers.py", line 641, in wrapper
    result = func(*args, **kwargs)
  File "/.../RecordFlux/rflx/expression.py", line 1797, in substituted
    expr = func(self)
  File "/.../RecordFlux/rflx/generator/session.py", line 3700, in func
    assert len(expression.elements) > 0
AssertionError
@jklmnn jklmnn added bug specification Related to specification package (e.g., specification parsing) labels Aug 19, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug specification Related to specification package (e.g., specification parsing)
Projects
None yet
Development

No branches or pull requests

1 participant