Issue 796: Add function for getting current state of session

[treiher]

• Closes Retrieve current state from session #796

[senier]

@treiher I wonder whether we should remove the built-in debug output from RecordFlux as printing the states can now be easily done using the Tick interface?

[treiher]

Yes, that makes sense. I have created an issue for this purpose: #801.

[treiher]

For some reason the verification of the DHCP Client example fails:

gnatprove -Pdhcp_client
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

rflx-dhcp_client-session.adb:190:24: medium: precondition might fail, cannot prove Field_First (Ctx, F_Parameter_Request_List) mod RFLX_Types.Byte'Size = 1, in instantiation at session.ads:7
  190 |            DHCP.Option.Set_Parameter_Request_List (RFLX_Element_Options_Ctx, Parameter_Request_List_Ctx);
      |            ~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The affected code is unrelated to the changes of this PR. We have seen the same issue before:

#789 (comment)
https://github.com/Componolit/RecordFlux/runs/3762524957?check_suite_focus=true

But rerunning the jobs did not help this time.

Also, the Python ping test fails occasionally (only in the FSF GNAT job; rerunning the jobs sometimes helps here):

make -C examples/apps/ping test_python
make[1]: Entering directory '/home/runner/work/RecordFlux/RecordFlux/examples/apps/ping'
sudo -n timeout 3 `which python3` ping.py 127.0.0.1 | grep -q "64 bytes from 127.0.0.1: icmp_seq=0"
make[1]: *** [Makefile:10: test_python] Error 1
make[1]: Leaving directory '/home/runner/work/RecordFlux/RecordFlux/examples/apps/ping'
make: *** [Makefile:102: test_apps] Error 2

I cannot reproduce these issues locally.