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.

Sign up for GitHub

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

Issue 1155: Make In_IO_State function public #1157

Merged
merged 2 commits into from
Aug 29, 2022
Merged

Issue 1155: Make In_IO_State function public #1157

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
091f0df
Make In_IO_State function public
senier Aug 25, 2022
304f5dc
Further increase proof timeout for DHCP client
senier Aug 29, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ Generator:
- Add precondition `Uninitialized` to procedure `Initialize` (#788)
- Add operators for `Length` and `Index` types (#1070)
- Overwrite symlinks when creating files
- Make `In_IO_State` session function public (#1155)

PyRFLX:

Expand Down
2 changes: 1 addition & 1 deletion examples/apps/dhcp_client/dhcp_client.gpr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ project DHCP_Client is

package Prove is
for Proof_Switches ("Ada") use Defaults.Proof_Switches;
for Proof_Switches ("rflx-dhcp_client-session.adb") use ("--timeout=420");
for Proof_Switches ("rflx-dhcp_client-session.adb") use ("--timeout=450");
end Prove;

end DHCP_Client;
42 changes: 27 additions & 15 deletions rflx/generator/session.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,7 +357,8 @@ def is_global(identifier: ID) -> bool:
unit += self._create_reset_messages_before_write_procedure(self._session, is_global)

unit += self._create_tick_procedure(self._session, has_reads)
unit += self._create_run_procedure(self._session)
unit += self._create_in_io_state_function(self._session)
unit += self._create_run_procedure()
unit += self._create_state_function()

if has_writes:
Expand Down Expand Up @@ -1134,7 +1135,7 @@ def _create_tick_procedure(self, session: model.Session, has_writes: bool) -> Un
)

@staticmethod
def _create_run_procedure(session: model.Session) -> UnitPart:
def _create_in_io_state_function(session: model.Session) -> UnitPart:
io_states = [
state
for state in session.states
Expand All @@ -1148,6 +1149,30 @@ def _create_run_procedure(session: model.Session) -> UnitPart:
)
)
]
in_io_state_specification = FunctionSpecification(
"In_IO_State",
"Boolean",
[Parameter(["Ctx" if io_states else "Unused_Ctx"], "Context'Class")],
)
return UnitPart(
[
SubprogramDeclaration(in_io_state_specification),
],
[
ExpressionFunctionDeclaration(
in_io_state_specification,
In(
Variable("Ctx.P.Next_State"),
ChoiceList(*[Variable(f"S_{state.identifier}") for state in io_states]),
)
if io_states
else FALSE,
),
],
)

@staticmethod
def _create_run_procedure() -> UnitPart:
specification = ProcedureSpecification("Run", [InOutParameter(["Ctx"], "Context'Class")])
return UnitPart(
[
Expand All @@ -1162,19 +1187,6 @@ def _create_run_procedure(session: model.Session) -> UnitPart:
Pragma("Warnings", [Variable("On"), String('subprogram "Run" has no effect')]),
],
[
ExpressionFunctionDeclaration(
FunctionSpecification(
"In_IO_State",
"Boolean",
[Parameter(["Ctx" if io_states else "Unused_Ctx"], "Context'Class")],
),
In(
Variable("Ctx.P.Next_State"),
ChoiceList(*[Variable(f"S_{state.identifier}") for state in io_states]),
)
if io_states
else FALSE,
),
SubprogramBody(
specification,
[],
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/messages_with_implict_size/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/messages_with_single_opaque_field/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/parameterized_messages/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_append_unconstrained/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_binding/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_case_expression_aggregate/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_case_expression_numeric/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_channel_multiplexing/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_channels/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_comprehension_head/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_conversion/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_endianness/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_functions/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_functions_opaque/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Unused_Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_integration/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_integration_multiple/generated/rflx-b-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_integration_multiple/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_minimal/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_reuse_of_message/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_sequence_append/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_sequence_append_head/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_setting_of_message_fields/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_simple/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down
2 changes: 2 additions & 0 deletions tests/integration/session_variable_initialization/generated/rflx-test-session.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ is

pragma Warnings (On, "subprogram ""Tick"" has no effect");

function In_IO_State (Ctx : Context'Class) return Boolean;

pragma Warnings (Off, "subprogram ""Run"" has no effect");

procedure Run (Ctx : in out Context'Class) with
Expand Down