heisenbugltd/spat

SPARK Proof Analysis Tool

spat's Issues

Provide an entity filter parameter

When trying to analyze single proof times, the current filters are not sufficient. An idea would be to add some entity filter option to only show matching entries for a certain entity.

Roughly like

run_spat -rf - ct -e Setup_Key -P saatana.gpr

Which would have the expected effect (report failed/sort by time), but only for entities that match "Setup_Key".

Open questions: Maybe wildcard matching, or even reg exp?

Suggested configuration is incomplete

Describe the bug
I have run SPAT (run_spat V1.1.1 (compiled by SYSTEM_NAME_GNAT Community 2020 (20200429-93))) on RecordFlux´s test suite and found the following issues:

1. For multiple units (e.g., rflx-rflx_types) no prover configuration is generated. SPAT shows information for this unit in the summary and thus should be able to create a configuration for it.

rflx-rflx_types.spark                     => (Flow  => 37.8 ms,
                                              Proof => 29.8 s/60.0 s/714.0 s)

2. Multiple prover configurations are generated for generics. (I suppose Proof_Switches has no effect on generic packages.)

   for Proof_Switches ("rflx-rflx_generic_types.adb") use ("--prover=CVC4,altergo", "--steps=239854", "--timeout=30");
   for Proof_Switches ("rflx-rflx_generic_types.ads") use ("--prover=CVC4,altergo", "--steps=364532", "--timeout=58");
   for Proof_Switches ("rflx-rflx_generic_types.ads") use ("--prover=CVC4,Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-rflx_generic_types.ads") use ("--prover=CVC4,Z3", "--steps=11566", "--timeout=10");

Console Output

$ run_spat -Ptest.gpr --suggest --verbose
Debug: GNAT project loaded in 36.7 ms.
Debug: Found "rflx-arrays-av_enumeration_vector.ads"...Debug: "rflx-arrays-av_enumeration_vector.spark" added to index.
Debug: Found "rflx-arrays-enumeration_vector.ads"...Debug: "rflx-arrays-enumeration_vector.spark" added to index.
Debug: Found "rflx-arrays-generic_inner_message.adb"...Debug: "rflx-arrays-generic_inner_message.spark" not found on disk, skipped.
Debug: Found "rflx-arrays-generic_inner_message.ads"...Debug: "rflx-arrays-generic_inner_message.spark" already in index.
Debug: Found "rflx-arrays-generic_message.adb"...Debug: "rflx-arrays-generic_message.spark" not found on disk, skipped.
Debug: Found "rflx-arrays-generic_message.ads"...Debug: "rflx-arrays-generic_message.spark" already in index.
Debug: Found "rflx-arrays-generic_messages_message.adb"...Debug: "rflx-arrays-generic_messages_message.spark" not found on disk, skipped.
Debug: Found "rflx-arrays-generic_messages_message.ads"...Debug: "rflx-arrays-generic_messages_message.spark" already in index.
Debug: Found "rflx-arrays-inner_message.ads"...Debug: "rflx-arrays-inner_message.spark" added to index.
Debug: Found "rflx-arrays-inner_messages.ads"...Debug: "rflx-arrays-inner_messages.spark" added to index.
Debug: Found "rflx-arrays-message.ads"...Debug: "rflx-arrays-message.spark" added to index.
Debug: Found "rflx-arrays-messages_message.ads"...Debug: "rflx-arrays-messages_message.spark" added to index.
Debug: Found "rflx-arrays-modular_vector.ads"...Debug: "rflx-arrays-modular_vector.spark" added to index.
Debug: Found "rflx-arrays-range_vector.ads"...Debug: "rflx-arrays-range_vector.spark" added to index.
Debug: Found "rflx-arrays.ads"...Debug: "rflx-arrays.spark" added to index.
Debug: Found "rflx-derivation-message.ads"...Debug: "rflx-derivation-message.spark" added to index.
Debug: Found "rflx-derivation.ads"...Debug: "rflx-derivation.spark" added to index.
Debug: Found "rflx-enumeration-generic_message.adb"...Debug: "rflx-enumeration-generic_message.spark" not found on disk, skipped.
Debug: Found "rflx-enumeration-generic_message.ads"...Debug: "rflx-enumeration-generic_message.spark" already in index.
Debug: Found "rflx-enumeration-message.ads"...Debug: "rflx-enumeration-message.spark" added to index.
Debug: Found "rflx-enumeration.ads"...Debug: "rflx-enumeration.spark" added to index.
Debug: Found "rflx-ethernet-frame.ads"...Debug: "rflx-ethernet-frame.spark" added to index.
Debug: Found "rflx-ethernet-generic_frame.adb"...Debug: "rflx-ethernet-generic_frame.spark" not found on disk, skipped.
Debug: Found "rflx-ethernet-generic_frame.ads"...Debug: "rflx-ethernet-generic_frame.spark" already in index.
Debug: Found "rflx-ethernet.ads"...Debug: "rflx-ethernet.spark" added to index.
Debug: Found "rflx-expression-generic_message.adb"...Debug: "rflx-expression-generic_message.spark" not found on disk, skipped.
Debug: Found "rflx-expression-generic_message.ads"...Debug: "rflx-expression-generic_message.spark" already in index.
Debug: Found "rflx-expression-message.ads"...Debug: "rflx-expression-message.spark" added to index.
Debug: Found "rflx-expression.ads"...Debug: "rflx-expression.spark" added to index.
Debug: Found "rflx-in_ethernet-contains.ads"...Debug: "rflx-in_ethernet-contains.spark" added to index.
Debug: Found "rflx-in_ethernet-generic_contains.adb"...Debug: "rflx-in_ethernet-generic_contains.spark" not found on disk, skipped.
Debug: Found "rflx-in_ethernet-generic_contains.ads"...Debug: "rflx-in_ethernet-generic_contains.spark" already in index.
Debug: Found "rflx-in_ethernet.ads"...Debug: "rflx-in_ethernet.spark" added to index.
Debug: Found "rflx-in_ipv4-contains.ads"...Debug: "rflx-in_ipv4-contains.spark" added to index.
Debug: Found "rflx-in_ipv4-generic_contains.adb"...Debug: "rflx-in_ipv4-generic_contains.spark" not found on disk, skipped.
Debug: Found "rflx-in_ipv4-generic_contains.ads"...Debug: "rflx-in_ipv4-generic_contains.spark" already in index.
Debug: Found "rflx-in_ipv4.ads"...Debug: "rflx-in_ipv4.spark" added to index.
Debug: Found "rflx-in_tlv-contains.ads"...Debug: "rflx-in_tlv-contains.spark" added to index.
Debug: Found "rflx-in_tlv-generic_contains.ads"...Debug: "rflx-in_tlv-generic_contains.spark" not found on disk, skipped.
Debug: Found "rflx-in_tlv.ads"...Debug: "rflx-in_tlv.spark" added to index.
Debug: Found "rflx-ipv4-generic_option.adb"...Debug: "rflx-ipv4-generic_option.spark" not found on disk, skipped.
Debug: Found "rflx-ipv4-generic_option.ads"...Debug: "rflx-ipv4-generic_option.spark" already in index.
Debug: Found "rflx-ipv4-generic_packet.adb"...Debug: "rflx-ipv4-generic_packet.spark" not found on disk, skipped.
Debug: Found "rflx-ipv4-generic_packet.ads"...Debug: "rflx-ipv4-generic_packet.spark" already in index.
Debug: Found "rflx-ipv4-option.ads"...Debug: "rflx-ipv4-option.spark" added to index.
Debug: Found "rflx-ipv4-options.ads"...Debug: "rflx-ipv4-options.spark" added to index.
Debug: Found "rflx-ipv4-packet.ads"...Debug: "rflx-ipv4-packet.spark" added to index.
Debug: Found "rflx-ipv4.ads"...Debug: "rflx-ipv4.spark" added to index.
Debug: Found "rflx-rflx_arithmetic.adb"...Debug: "rflx-rflx_arithmetic.spark" added to index.
Debug: Found "rflx-rflx_arithmetic.ads"...Debug: "rflx-rflx_arithmetic.spark" already in index.
Debug: Found "rflx-rflx_builtin_types-conversions.ads"...Debug: "rflx-rflx_builtin_types-conversions.spark" added to index.
Debug: Found "rflx-rflx_builtin_types.ads"...Debug: "rflx-rflx_builtin_types.spark" added to index.
Debug: Found "rflx-rflx_generic_types.adb"...Debug: "rflx-rflx_generic_types.spark" not found on disk, skipped.
Debug: Found "rflx-rflx_generic_types.ads"...Debug: "rflx-rflx_generic_types.spark" already in index.
Debug: Found "rflx-rflx_message_sequence.adb"...Debug: "rflx-rflx_message_sequence.spark" not found on disk, skipped.
Debug: Found "rflx-rflx_message_sequence.ads"...Debug: "rflx-rflx_message_sequence.spark" already in index.
Debug: Found "rflx-rflx_scalar_sequence.adb"...Debug: "rflx-rflx_scalar_sequence.spark" not found on disk, skipped.
Debug: Found "rflx-rflx_scalar_sequence.ads"...Debug: "rflx-rflx_scalar_sequence.spark" already in index.
Debug: Found "rflx-rflx_types.ads"...Debug: "rflx-rflx_types.spark" added to index.
Debug: Found "rflx-tlv-generic_message.adb"...Debug: "rflx-tlv-generic_message.spark" not found on disk, skipped.
Debug: Found "rflx-tlv-generic_message.ads"...Debug: "rflx-tlv-generic_message.spark" already in index.
Debug: Found "rflx-tlv-message.ads"...Debug: "rflx-tlv-message.spark" added to index.
Debug: Found "rflx-tlv.ads"...Debug: "rflx-tlv.spark" added to index.
Debug: Found "rflx-udp-datagram.ads"...Debug: "rflx-udp-datagram.spark" added to index.
Debug: Found "rflx-udp-generic_datagram.adb"...Debug: "rflx-udp-generic_datagram.spark" not found on disk, skipped.
Debug: Found "rflx-udp-generic_datagram.ads"...Debug: "rflx-udp-generic_datagram.spark" already in index.
Debug: Found "rflx-udp.ads"...Debug: "rflx-udp.spark" added to index.
Debug: Found "rflx.ads"...Debug: "rflx.spark" added to index.
Debug: Found "ethernet.rflx"...Debug: "ethernet.spark" not found on disk, skipped.
Debug: Found "icmp.rflx"...Debug: "icmp.spark" not found on disk, skipped.
Debug: Found "in_ethernet.rflx"...Debug: "in_ethernet.spark" not found on disk, skipped.
Debug: Found "in_ipv4.rflx"...Debug: "in_ipv4.spark" not found on disk, skipped.
Debug: Found "ipv4.rflx"...Debug: "ipv4.spark" not found on disk, skipped.
Debug: Found "test.rflx"...Debug: "test.spark" added to index.
Debug: Found "tls_alert.rflx"...Debug: "tls_alert.spark" not found on disk, skipped.
Debug: Found "tls_handshake.rflx"...Debug: "tls_handshake.spark" not found on disk, skipped.
Debug: Found "tls_heartbeat.rflx"...Debug: "tls_heartbeat.spark" not found on disk, skipped.
Debug: Found "tls_record.rflx"...Debug: "tls_record.spark" not found on disk, skipped.
Debug: Found "tlv.rflx"...Debug: "tlv.spark" not found on disk, skipped.
Debug: Found "udp.rflx"...Debug: "udp.spark" not found on disk, skipped.
Debug: Found "array_message.rflx"...Debug: "array_message.spark" not found on disk, skipped.
Debug: Found "array_type.rflx"...Debug: "array_type.spark" not found on disk, skipped.
Debug: Found "comment_only.rflx"...Debug: "comment_only.spark" not found on disk, skipped.
Debug: Found "context.rflx"...Debug: "context.spark" not found on disk, skipped.
Debug: Found "context_cycle.rflx"...Debug: "context_cycle.spark" not found on disk, skipped.
Debug: Found "context_cycle_1.rflx"...Debug: "context_cycle_1.spark" not found on disk, skipped.
Debug: Found "context_cycle_2.rflx"...Debug: "context_cycle_2.spark" not found on disk, skipped.
Debug: Found "context_cycle_3.rflx"...Debug: "context_cycle_3.spark" not found on disk, skipped.
Debug: Found "duplicate_type.rflx"...Debug: "duplicate_type.spark" not found on disk, skipped.
Debug: Found "empty_file.rflx"...Debug: "empty_file.spark" not found on disk, skipped.
Debug: Found "empty_package.rflx"...Debug: "empty_package.spark" not found on disk, skipped.
Debug: Found "enumeration_type.rflx"...Debug: "enumeration_type.spark" not found on disk, skipped.
Debug: Found "feature_integration.rflx"...Debug: "feature_integration.spark" not found on disk, skipped.
Debug: Found "identical_literals.rflx"...Debug: "identical_literals.spark" not found on disk, skipped.
Debug: Found "incorrect_name.rflx"...Debug: "incorrect_name.spark" not found on disk, skipped.
Debug: Found "incorrect_specification.rflx"...Debug: "incorrect_specification.spark" not found on disk, skipped.
Debug: Found "integer_type.rflx"...Debug: "integer_type.spark" not found on disk, skipped.
Debug: Found "message_in_message.rflx"...Debug: "message_in_message.spark" not found on disk, skipped.
Debug: Found "message_odd_length.rflx"...Debug: "message_odd_length.spark" not found on disk, skipped.
Debug: Found "message_type.rflx"...Debug: "message_type.spark" not found on disk, skipped.
Debug: Found "null_message.rflx"...Debug: "null_message.spark" not found on disk, skipped.
Debug: Found "rflx-arrays-tests.adb"...Debug: "rflx-arrays-tests.spark" added to index.
Debug: Found "rflx-arrays-tests.ads"...Debug: "rflx-arrays-tests.spark" already in index.
Debug: Found "rflx-builtin_types_tests.adb"...Debug: "rflx-builtin_types_tests.spark" added to index.
Debug: Found "rflx-builtin_types_tests.ads"...Debug: "rflx-builtin_types_tests.spark" already in index.
Debug: Found "rflx-custom_types_tests.adb"...Debug: "rflx-custom_types_tests.spark" added to index.
Debug: Found "rflx-custom_types_tests.ads"...Debug: "rflx-custom_types_tests.spark" already in index.
Debug: Found "rflx-derivation-tests.adb"...Debug: "rflx-derivation-tests.spark" added to index.
Debug: Found "rflx-derivation-tests.ads"...Debug: "rflx-derivation-tests.spark" already in index.
Debug: Found "rflx-enumeration-tests.adb"...Debug: "rflx-enumeration-tests.spark" added to index.
Debug: Found "rflx-enumeration-tests.ads"...Debug: "rflx-enumeration-tests.spark" already in index.
Debug: Found "rflx-ethernet-tests.adb"...Debug: "rflx-ethernet-tests.spark" added to index.
Debug: Found "rflx-ethernet-tests.ads"...Debug: "rflx-ethernet-tests.spark" already in index.
Debug: Found "rflx-expression-tests.adb"...Debug: "rflx-expression-tests.spark" added to index.
Debug: Found "rflx-expression-tests.ads"...Debug: "rflx-expression-tests.spark" already in index.
Debug: Found "rflx-in_ethernet-tests.adb"...Debug: "rflx-in_ethernet-tests.spark" added to index.
Debug: Found "rflx-in_ethernet-tests.ads"...Debug: "rflx-in_ethernet-tests.spark" already in index.
Debug: Found "rflx-in_ipv4-tests.adb"...Debug: "rflx-in_ipv4-tests.spark" added to index.
Debug: Found "rflx-in_ipv4-tests.ads"...Debug: "rflx-in_ipv4-tests.spark" already in index.
Debug: Found "rflx-in_tlv-tests.adb"...Debug: "rflx-in_tlv-tests.spark" added to index.
Debug: Found "rflx-in_tlv-tests.ads"...Debug: "rflx-in_tlv-tests.spark" already in index.
Debug: Found "rflx-ipv4-tests.adb"...Debug: "rflx-ipv4-tests.spark" added to index.
Debug: Found "rflx-ipv4-tests.ads"...Debug: "rflx-ipv4-tests.spark" already in index.
Debug: Found "rflx-tlv-tests.adb"...Debug: "rflx-tlv-tests.spark" added to index.
Debug: Found "rflx-tlv-tests.ads"...Debug: "rflx-tlv-tests.spark" already in index.
Debug: Found "spark-assertions.adb"...Debug: "spark-assertions.spark" added to index.
Debug: Found "spark-assertions.ads"...Debug: "spark-assertions.spark" already in index.
Debug: Found "spark-file_io.adb"...Debug: "spark-file_io.spark" added to index.
Debug: Found "spark-file_io.ads"...Debug: "spark-file_io.spark" already in index.
Debug: Found "spark.ads"...Debug: "spark.spark" added to index.
Debug: Found "test.adb"...Debug: "test.spark" already in index.
Debug: Found "test_suite.adb"...Debug: "test_suite.spark" added to index.
Debug: Found "test_suite.ads"...Debug: "test_suite.spark" already in index.
Debug: Found "tlv_with_checksum.rflx"...Debug: "tlv_with_checksum.spark" not found on disk, skipped.
Debug: Found "type_refinement.rflx"...Debug: "type_refinement.spark" not found on disk, skipped.
Debug: Found "ada_containers-aunit_lists.adb"...Debug: "ada_containers-aunit_lists.spark" not found on disk, skipped.
Debug: Found "ada_containers-aunit_lists.ads"...Debug: "ada_containers-aunit_lists.spark" already in index.
Debug: Found "ada_containers.ads"...Debug: "ada_containers.spark" not found on disk, skipped.
Debug: Found "aunit-assertions-assert_exception.adb"...Debug: "aunit-assertions-assert_exception.spark" not found on disk, skipped.
Debug: Found "aunit-assertions.adb"...Debug: "aunit-assertions.spark" not found on disk, skipped.
Debug: Found "aunit-assertions.ads"...Debug: "aunit-assertions.spark" already in index.
Debug: Found "aunit-memory-utils.adb"...Debug: "aunit-memory-utils.spark" not found on disk, skipped.
Debug: Found "aunit-memory-utils.ads"...Debug: "aunit-memory-utils.spark" already in index.
Debug: Found "aunit-memory.adb"...Debug: "aunit-memory.spark" not found on disk, skipped.
Debug: Found "aunit-memory.ads"...Debug: "aunit-memory.spark" already in index.
Debug: Found "aunit-options.ads"...Debug: "aunit-options.spark" not found on disk, skipped.
Debug: Found "aunit-reporter-gnattest.adb"...Debug: "aunit-reporter-gnattest.spark" not found on disk, skipped.
Debug: Found "aunit-reporter-gnattest.ads"...Debug: "aunit-reporter-gnattest.spark" already in index.
Debug: Found "aunit-reporter-text.adb"...Debug: "aunit-reporter-text.spark" not found on disk, skipped.
Debug: Found "aunit-reporter-text.ads"...Debug: "aunit-reporter-text.spark" already in index.
Debug: Found "aunit-reporter-xml.adb"...Debug: "aunit-reporter-xml.spark" not found on disk, skipped.
Debug: Found "aunit-reporter-xml.ads"...Debug: "aunit-reporter-xml.spark" already in index.
Debug: Found "aunit-reporter.ads"...Debug: "aunit-reporter.spark" not found on disk, skipped.
Debug: Found "aunit-run.adb"...Debug: "aunit-run.spark" not found on disk, skipped.
Debug: Found "aunit-run.ads"...Debug: "aunit-run.spark" already in index.
Debug: Found "aunit-simple_test_cases-run_routine.adb"...Debug: "aunit-simple_test_cases-run_routine.spark" not found on disk, skipped.
Debug: Found "aunit-simple_test_cases.adb"...Debug: "aunit-simple_test_cases.spark" not found on disk, skipped.
Debug: Found "aunit-simple_test_cases.ads"...Debug: "aunit-simple_test_cases.spark" already in index.
Debug: Found "aunit-test_caller.adb"...Debug: "aunit-test_caller.spark" not found on disk, skipped.
Debug: Found "aunit-test_caller.ads"...Debug: "aunit-test_caller.spark" already in index.
Debug: Found "aunit-test_cases-call_set_up_case.adb"...Debug: "aunit-test_cases-call_set_up_case.spark" not found on disk, skipped.
Debug: Found "aunit-test_cases-registration.adb"...Debug: "aunit-test_cases-registration.spark" not found on disk, skipped.
Debug: Found "aunit-test_cases.adb"...Debug: "aunit-test_cases.spark" not found on disk, skipped.
Debug: Found "aunit-test_cases.ads"...Debug: "aunit-test_cases.spark" already in index.
Debug: Found "aunit-test_filters.adb"...Debug: "aunit-test_filters.spark" not found on disk, skipped.
Debug: Found "aunit-test_filters.ads"...Debug: "aunit-test_filters.spark" already in index.
Debug: Found "aunit-test_fixtures.adb"...Debug: "aunit-test_fixtures.spark" not found on disk, skipped.
Debug: Found "aunit-test_fixtures.ads"...Debug: "aunit-test_fixtures.spark" already in index.
Debug: Found "aunit-test_results.adb"...Debug: "aunit-test_results.spark" not found on disk, skipped.
Debug: Found "aunit-test_results.ads"...Debug: "aunit-test_results.spark" already in index.
Debug: Found "aunit-test_suites.adb"...Debug: "aunit-test_suites.spark" not found on disk, skipped.
Debug: Found "aunit-test_suites.ads"...Debug: "aunit-test_suites.spark" already in index.
Debug: Found "aunit-tests.ads"...Debug: "aunit-tests.spark" not found on disk, skipped.
Debug: Found "aunit-time_measure.adb"...Debug: "aunit-time_measure.spark" not found on disk, skipped.
Debug: Found "aunit-time_measure.ads"...Debug: "aunit-time_measure.spark" already in index.
Debug: Found "aunit.adb"...Debug: "aunit.spark" not found on disk, skipped.
Debug: Found "aunit.ads"...Debug: "aunit.spark" already in index.
Debug: Search completed in 1.7 ms, 53 files found.
Debug: Using up to 16 parsing threads.
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-av_enumeration_vector.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-enumeration_vector.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-inner_message.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-inner_messages.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-message.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-messages_message.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-modular_vector.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-range_vector.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation-message.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration-message.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet-frame.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-expression-message.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-expression.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet-contains.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4-contains.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_tlv-contains.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_tlv.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-option.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-options.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-packet.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_arithmetic.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_builtin_types-conversions.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_builtin_types.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_types.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv-message.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-udp-datagram.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-udp.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/test.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-builtin_types_tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-custom_types_tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-expression-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_tlv-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv-tests.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/spark-assertions.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/spark-file_io.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/spark.spark"...
Debug: Queuing "/home/tr/sync/RecordFlux/build/gnatprove/test_suite.spark"...
Debug: Picking up results...
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-expression.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_tlv-contains.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_tlv.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet-contains.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4-contains.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-inner_messages.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-options.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_builtin_types.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_builtin_types-conversions.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-av_enumeration_vector.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-modular_vector.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-enumeration_vector.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-range_vector.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/test.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-udp.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_arithmetic.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-expression-message.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration-message.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_types.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-expression-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-inner_message.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_tlv-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-messages_message.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-builtin_types_tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/spark-assertions.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/spark-file_io.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/spark.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/test_suite.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv-message.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation-message.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-udp-datagram.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-message.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet-tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-custom_types_tests.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-option.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet-frame.spark"...ok.
Debug: "/home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-packet.spark"...ok.
Debug: Parsing completed in 362.9 ms.
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: File version: GNAT_CE_2020
Debug: Reading completed in 566.3 ms.
Debug: Cut off point set to 0.0 s.
Warning: You requested a suggested prover configuration.
Warning: This feature is highly experimental.
Warning: Please consult the documentation.
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-option.spark
Debug:   CVC4
Debug:     t(Success) 2.9 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 1.4 s
Debug:     S(Success) 640
Debug:     file     "rflx-ipv4-generic_option.ads"
Debug:   Z3
Debug:     t(Success) 40.5 s
Debug:     t(Failed)  680.0 ms
Debug:     T(Success) 790.0 ms
Debug:     S(Success) 1979
Debug:     file     "rflx-ipv4-generic_option.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-udp-datagram.spark
Debug:   CVC4
Debug:     t(Success) 4.6 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 4.6 s
Debug:     S(Success) 2334
Debug:     file     "rflx-udp-generic_datagram.ads"
Debug:   Z3
Debug:     t(Success) 25.4 s
Debug:     t(Failed)  1.1 s
Debug:     T(Success) 460.0 ms
Debug:     S(Success) 1863
Debug:     file     "rflx-udp-generic_datagram.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation-tests.spark
Debug:   Z3
Debug:     t(Success) 33.3 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 1.1 s
Debug:     S(Success) 2215
Debug:     file     "rflx-derivation-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays.spark
Debug:   Z3
Debug:     t(Success) 150.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 20.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-arrays.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet-tests.spark
Debug:   Z3
Debug:     t(Success) 28.3 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 1.0 s
Debug:     S(Success) 3359
Debug:     file     "rflx-ethernet-generic_frame.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-expression-tests.spark
Debug:   Z3
Debug:     t(Success) 820.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 80.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-expression-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv-tests.spark
Debug:   Z3
Debug:     t(Success) 7.7 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 170.0 ms
Debug:     S(Success) 467
Debug:     file     "rflx-tlv-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet.spark
Debug:   Z3
Debug:     t(Success) 90.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 20.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-ethernet.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration-tests.spark
Debug:   Z3
Debug:     t(Success) 1.7 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 90.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-enumeration-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_arithmetic.spark
Debug:   altergo
Debug:     t(Success) 4.2 s
Debug:     t(Failed)  304.1 s
Debug:     T(Success) 381.7 ms
Debug:     S(Success) 3039
Debug:     file     "rflx-rflx_arithmetic.adb"
Debug:   CVC4
Debug:     t(Success) 137.6 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 50.3 s
Debug:     S(Success) 70979
Debug:     file     "rflx-rflx_arithmetic.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv.spark
Debug:   Z3
Debug:     t(Success) 60.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 20.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-tlv.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ethernet-frame.spark
Debug:   Z3
Debug:     t(Success) 74.7 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 3.6 s
Debug:     S(Success) 14670
Debug:     file     "rflx-ethernet-generic_frame.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-tlv-message.spark
Debug:   CVC4
Debug:     t(Success) 1.7 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 850.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-tlv-generic_message.adb"
Debug:   Z3
Debug:     t(Success) 13.7 s
Debug:     t(Failed)  450.0 ms
Debug:     T(Success) 130.0 ms
Debug:     S(Success) 109
Debug:     file     "rflx-tlv-generic_message.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-custom_types_tests.spark
Debug:   altergo
Debug:     t(Success) 851.6 s
Debug:     t(Failed)  1.6 ks
Debug:     T(Success) 57.9 s
Debug:     S(Success) 364532
Debug:     file     "rflx-rflx_generic_types.ads"
Debug:   CVC4
Debug:     t(Success) 268.2 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 48.5 s
Debug:     S(Success) 50012
Debug:     file     "rflx-rflx_generic_types.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-enumeration_vector.spark
Debug:   Z3
Debug:     t(Success) 1.9 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 120.0 ms
Debug:     S(Success) 247
Debug:     file     "rflx-rflx_scalar_sequence.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-tests.spark
Debug:   Z3
Debug:     t(Success) 44.0 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 680.0 ms
Debug:     S(Success) 1672
Debug:     file     "rflx-arrays-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-in_tlv-tests.spark
Debug:   Z3
Debug:     t(Success) 400.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 80.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-in_tlv-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-messages_message.spark
Debug:   CVC4
Debug:     t(Success) 840.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 840.0 ms
Debug:     S(Success) 633
Debug:     file     "rflx-arrays-generic_messages_message.ads"
Debug:   Z3
Debug:     t(Success) 9.9 s
Debug:     t(Failed)  460.0 ms
Debug:     T(Success) 240.0 ms
Debug:     S(Success) 618
Debug:     file     "rflx-arrays-generic_messages_message.adb"
Debug:   Trivial
Debug:     t(Success) 0.0 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 0.0 s
Debug:     S(Success) 1
Debug:     file     "rflx-arrays-generic_messages_message.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-packet.spark
Debug:   CVC4
Debug:     t(Success) 38.7 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 9.8 s
Debug:     S(Success) 11566
Debug:     file     "rflx-ipv4-generic_packet.ads"
Debug:   Z3
Debug:     t(Success) 281.9 s
Debug:     t(Failed)  19.8 s
Debug:     T(Success) 3.9 s
Debug:     S(Success) 10747
Debug:     file     "rflx-rflx_generic_types.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-message.spark
Debug:   CVC4
Debug:     t(Success) 3.1 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 1.1 s
Debug:     S(Success) 183
Debug:     file     "rflx-arrays-generic_message.adb"
Debug:   Z3
Debug:     t(Success) 26.9 s
Debug:     t(Failed)  790.0 ms
Debug:     T(Success) 280.0 ms
Debug:     S(Success) 540
Debug:     file     "rflx-arrays-generic_message.adb"
Debug:   Trivial
Debug:     t(Success) 0.0 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 0.0 s
Debug:     S(Success) 1
Debug:     file     "rflx-arrays-generic_message.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-inner_messages.spark
Debug:   Z3
Debug:     t(Success) 1.3 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 60.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-rflx_message_sequence.ads"
Debug:   Trivial
Debug:     t(Success) 0.0 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 0.0 s
Debug:     S(Success) 1
Debug:     file     "rflx-rflx_message_sequence.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration-message.spark
Debug:   Z3
Debug:     t(Success) 5.9 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 150.0 ms
Debug:     S(Success) 359
Debug:     file     "rflx-enumeration-generic_message.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-enumeration.spark
Debug:   Z3
Debug:     t(Success) 40.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 20.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-enumeration.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-tests.spark
Debug:   Z3
Debug:     t(Success) 69.6 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 13.3 s
Debug:     S(Success) 76924
Debug:     file     "rflx-ipv4-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4-options.spark
Debug:   Z3
Debug:     t(Success) 830.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 40.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-rflx_message_sequence.ads"
Debug:   Trivial
Debug:     t(Success) 0.0 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 0.0 s
Debug:     S(Success) 1
Debug:     file     "rflx-rflx_message_sequence.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-expression-message.spark
Debug:   Z3
Debug:     t(Success) 4.5 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 70.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-expression-generic_message.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-modular_vector.spark
Debug:   CVC4
Debug:     t(Success) 450.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 450.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-rflx_scalar_sequence.adb"
Debug:   Z3
Debug:     t(Success) 1.7 s
Debug:     t(Failed)  140.0 ms
Debug:     T(Success) 70.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-rflx_generic_types.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-derivation-message.spark
Debug:   CVC4
Debug:     t(Success) 3.2 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 1.1 s
Debug:     S(Success) 183
Debug:     file     "rflx-arrays-generic_message.ads"
Debug:   Z3
Debug:     t(Success) 27.1 s
Debug:     t(Failed)  800.0 ms
Debug:     T(Success) 280.0 ms
Debug:     S(Success) 530
Debug:     file     "rflx-arrays-generic_message.ads"
Debug:   Trivial
Debug:     t(Success) 0.0 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 0.0 s
Debug:     S(Success) 1
Debug:     file     "rflx-arrays-generic_message.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-range_vector.spark
Debug:   Z3
Debug:     t(Success) 2.0 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 140.0 ms
Debug:     S(Success) 446
Debug:     file     "rflx-rflx_scalar_sequence.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4-tests.spark
Debug:   Z3
Debug:     t(Success) 218.1 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 34.5 s
Debug:     S(Success) 141142
Debug:     file     "rflx-in_ipv4-tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-builtin_types_tests.spark
Debug:   Z3
Debug:     t(Success) 10.6 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 60.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-builtin_types_tests.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet-contains.spark
Debug:   CVC4
Debug:     t(Success) 1.7 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 1.7 s
Debug:     S(Success) 521
Debug:     file     "rflx-in_ethernet-generic_contains.ads"
Debug:   Z3
Debug:     t(Success) 1.3 s
Debug:     t(Failed)  350.0 ms
Debug:     T(Success) 340.0 ms
Debug:     S(Success) 449
Debug:     file     "rflx-in_ethernet-generic_contains.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-rflx_types.spark
Debug:   altergo
Debug:     t(Success) 207.9 s
Debug:     t(Failed)  316.6 s
Debug:     T(Success) 29.2 s
Debug:     S(Success) 239854
Debug:     file     "rflx-rflx_generic_types.adb"
Debug:   CVC4
Debug:     t(Success) 75.5 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 29.8 s
Debug:     S(Success) 40212
Debug:     file     "rflx-rflx_generic_types.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ethernet-tests.spark
Debug:   Z3
Debug:     t(Success) 134.4 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 28.8 s
Debug:     S(Success) 108032
Debug:     file     "rflx-ipv4-generic_packet.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-udp.spark
Debug:   Z3
Debug:     t(Success) 70.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 30.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-udp.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-av_enumeration_vector.spark
Debug:   Z3
Debug:     t(Success) 1.9 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 160.0 ms
Debug:     S(Success) 683
Debug:     file     "rflx-rflx_scalar_sequence.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-in_ipv4-contains.spark
Debug:   CVC4
Debug:     t(Success) 24.6 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 24.6 s
Debug:     S(Success) 117158
Debug:     file     "rflx-in_ipv4-generic_contains.ads"
Debug:   Z3
Debug:     t(Success) 1.9 s
Debug:     t(Failed)  35.4 s
Debug:     T(Success) 500.0 ms
Debug:     S(Success) 585
Debug:     file     "rflx-in_ipv4-generic_contains.adb"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-ipv4.spark
Debug:   Z3
Debug:     t(Success) 300.0 ms
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 20.0 ms
Debug:     S(Success) 1
Debug:     file     "rflx-ipv4.ads"
Debug: /home/tr/sync/RecordFlux/build/gnatprove/rflx-arrays-inner_message.spark
Debug:   Z3
Debug:     t(Success) 8.9 s
Debug:     t(Failed)  0.0 s
Debug:     T(Success) 180.0 ms
Debug:     S(Success) 338
Debug:     file     "rflx-arrays-generic_inner_message.adb"

package Prove is
   for Proof_Switches ("rflx-arrays-generic_inner_message.adb") use ("--prover=Z3", "--steps=338", "--timeout=1");
   for Proof_Switches ("rflx-arrays-generic_message.ads") use ("--prover=CVC4,Z3", "--steps=530", "--timeout=2");
   for Proof_Switches ("rflx-arrays-generic_message.ads") use ("--prover=CVC4,Z3", "--steps=540", "--timeout=2");
   for Proof_Switches ("rflx-arrays-generic_messages_message.ads") use ("--prover=CVC4,Z3", "--steps=633", "--timeout=1");
   for Proof_Switches ("rflx-arrays-tests.adb") use ("--prover=Z3", "--steps=1672", "--timeout=1");
   for Proof_Switches ("rflx-arrays.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-builtin_types_tests.adb") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-derivation-tests.adb") use ("--prover=Z3", "--steps=2215", "--timeout=2");
   for Proof_Switches ("rflx-enumeration-generic_message.ads") use ("--prover=Z3", "--steps=359", "--timeout=1");
   for Proof_Switches ("rflx-enumeration-tests.adb") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-enumeration.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-ethernet-generic_frame.adb") use ("--prover=Z3", "--steps=14670", "--timeout=4");
   for Proof_Switches ("rflx-ethernet-generic_frame.ads") use ("--prover=Z3", "--steps=3359", "--timeout=1");
   for Proof_Switches ("rflx-ethernet.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-expression-generic_message.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-expression-tests.adb") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-in_ethernet-generic_contains.ads") use ("--prover=CVC4,Z3", "--steps=521", "--timeout=2");
   for Proof_Switches ("rflx-in_ipv4-generic_contains.ads") use ("--prover=CVC4,Z3", "--steps=117158", "--timeout=25");
   for Proof_Switches ("rflx-in_ipv4-tests.adb") use ("--prover=Z3", "--steps=141142", "--timeout=35");
   for Proof_Switches ("rflx-in_tlv-tests.adb") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-ipv4-generic_option.ads") use ("--prover=CVC4,Z3", "--steps=1979", "--timeout=2");
   for Proof_Switches ("rflx-ipv4-generic_packet.ads") use ("--prover=Z3", "--steps=108032", "--timeout=29");
   for Proof_Switches ("rflx-ipv4-tests.adb") use ("--prover=Z3", "--steps=76924", "--timeout=14");
   for Proof_Switches ("rflx-ipv4.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--prover=CVC4,altergo", "--steps=70979", "--timeout=51");
   for Proof_Switches ("rflx-rflx_generic_types.adb") use ("--prover=CVC4,altergo", "--steps=239854", "--timeout=30");
   for Proof_Switches ("rflx-rflx_generic_types.ads") use ("--prover=CVC4,altergo", "--steps=364532", "--timeout=58");
   for Proof_Switches ("rflx-rflx_generic_types.ads") use ("--prover=CVC4,Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-rflx_generic_types.ads") use ("--prover=CVC4,Z3", "--steps=11566", "--timeout=10");
   for Proof_Switches ("rflx-rflx_message_sequence.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-rflx_message_sequence.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-rflx_scalar_sequence.adb") use ("--prover=Z3", "--steps=247", "--timeout=1");
   for Proof_Switches ("rflx-rflx_scalar_sequence.adb") use ("--prover=Z3", "--steps=446", "--timeout=1");
   for Proof_Switches ("rflx-rflx_scalar_sequence.adb") use ("--prover=Z3", "--steps=683", "--timeout=1");
   for Proof_Switches ("rflx-tlv-generic_message.ads") use ("--prover=CVC4,Z3", "--steps=109", "--timeout=1");
   for Proof_Switches ("rflx-tlv-tests.adb") use ("--prover=Z3", "--steps=467", "--timeout=1");
   for Proof_Switches ("rflx-tlv.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
   for Proof_Switches ("rflx-udp-generic_datagram.ads") use ("--prover=CVC4,Z3", "--steps=2334", "--timeout=5");
   for Proof_Switches ("rflx-udp.ads") use ("--prover=Z3", "--steps=1", "--timeout=1");
end Prove;

Improve (scale, extend) timeout values in suggested configuration

Is your feature request related to a problem? Please describe.

If you use the --suggest switch, the resulting suggested timeouts are rather optimistic and fragile. For instance, if a proof takes 1.9 seconds in the run that spat analysed, the suggested timeout configuration is --timeout=2 (essentially the ceiling value). Even if you run the proof always on the same machine dedicated only for proofs, times are in no way guaranteed due to different load, task scheduling, occasionally running background jobs, etc. pp. Cutting it so close may lead to random proof failures when using that configuration.

This also warrants an explanation in the documentation, so that the user is at least be made more aware of this.

Describe the solution you'd like

Suggested timeout values should have a (constant) minimum value to cater for load variations on the proofing machine and should be scaled by some percentage on the upper end. Roughly like:

Timeout_Value := (Maximum_Proof_Time (VC) + Min_Timeout) * 1.1; -- force a minimum time out and add 10% slack

For special needs such parameters could maybe also be passed on the command line to override the internal defaults.

Describe alternatives you've considered

Well, you can always do rough calculations like that manually, but this is error-prone and not user-friendly. This might be fine for "toy" projects with maybe a dozen of files, but becomes infeasible with larger project with many files.

Additional context

As a bare minimum, the proof time which was used for calculating the timeout should be added as a comment after the Proof_Switches line. That way, the user has at least an idea, how close the value to the timeout actually is. It makes no sense to increase a timeout to five seconds or so by default, if the maximum proof time is in the order of a couple of milliseconds.
Chances are, it will never ever come close to running for a whole second. It's a whole different case, if the recorded proof time is already 980 ms, then it is almost a certainty it will exceed a one second limit at some time. Right now, spat handles both cases as if they were the same.

Improve performance

Right now, when printing entities filtered by --failed or --unproved, the decision if the entity's proof tree has failed attempts results in multiple calls to Has_Failed_Attempts, Is_Unproved which each cause more similar calls into all dependent objects. This should be optimized, so that such properties are only calculated once.

For further discussion see this wiki-page

Support GNAT project files

We are already using GNATCOLL and the files we parse are rather GNAT specific, so to be in line with other tools, we could just as well use a .gpr file as input instead of wildly scanning directories. This is especially important as specifying the object directory to parse also catches files from the saved_runs subdirectory, causing inconsistent behaviour by including data from earlier runs. Parsing the project files and selectively finding the associated .spark should be more user friendly.

Sorting is not deterministic

See below for the reoccurence

---

The fix for issue #13 revealed that sorting is not stable.

In case of sorting by time, when two times are identical, we also need to take the entity name/source location into account, I'm afraid.

For VCs, the total_proof_time, the maximum_proof time and then the entity location should be compared.

It's a bit unclear what to do with single proof paths, though. They all reference the same location and entity, even sorting by prover name could result in undeterministic behaviour.

No 'diff' command on any of our build images

Currently the automated tests do not do the template comparison, because there is no diff on these images (i.e. diffutils not installed?)

Show minimum required time for successful proof

Is your feature request related to a problem? Please describe.
I want to improve the proof time for already known correct code. One way to achieve that is reducing the timeout to reduce wasting time on a prover which is unable to prove a certain VC. Unfortunately, the current output of SPAT does not allow getting the minimum required time easily. It may can be determined manually by using the details option, but that is quite tedious.

Here is an example of the current output:

RFLX.RFLX_Types.U64_Insert => 120.0 s/1.6 ks
`-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 120.0 s/491.0 s
 `-CVC4: 120.0 s (Timeout)
  -Z3: 120.0 s (Timeout)
  -altergo: 188.2 ms (Valid)
 `-Z3: 120.0 s (Timeout)
  -CVC4: 5.4 s (Valid)
 `-Z3: 120.0 s (Timeout)
  -CVC4: 5.3 s (Valid)
 `-Z3: 60.0 ms (Valid)
 `-Z3: 40.0 ms (Valid)
 `-Z3: 20.0 ms (Valid)
 `-Trivial: 0.0 s (Valid)

SPAT shows a very high maximum time used by a prover (120.0 s), while it cannot be seen easily that the required time could be reduced significantly when reducing the timeout (5.4 s + some buffer for the shown VC).

Describe the solution you'd like
It would be nice if the output could be extended by a value for the maximum time needed by any prover for a valid proof. For example:

RFLX.RFLX_Types.U64_Insert => 5.4 s/120.0 s/1.6 ks
`-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 5.4 s/120.0 s/491.0 s
[...]

It would be also helpful to be able to sort the output by this value, so that the maximum value for the whole project can be easily seen.

Document in README that tool must be used on pristine run of GNATprove

SPAT will only work as intended after a run from scratch of GNATprove, not on a subsequent run. Indeed, on subsequent runs, GNATprove will regenerate .spark files but spend no time on checks that were already proved, or even in some cases no time on any checks (if switch --output-msg-only is used). As a result, the time info for most check is just "0.0 s".

This should be described in the README, so that users are not surprised.

The underlying reason for that behavior of GNATprove is that the Why3 session files are where all the history of prover runs and current state is stored. A reasonable solution to improve the connection between GNATprove and SPAT would be to regenerate the timing information in .spark files from the info read in the Why3 session files. Feel free to open an Issue on spark2014 repo if you'd like us to investigate it!

Option --cut-off and --sort-by=s don't work as one may expect (documented as is)

Describe the bug
As described in the README.md, the --cut-off option works for maximal proof time, not for maximum time for successful proof.

Expected Behavior
If one requests sorting by maximum time for successful proof, the --cut-off should take that parameter into account.

GNATStudio plugin

It could be handy to have a plug-in in GNATStudio so that the user can run the tool after a prove and see the information possibly interspersed with the actual source code.

Not clear yet, though, how the output should be displayed in the IDE.

Prepare SPAT for when step scaling becomes obsolete

Describe the bug
Currently we output scaled steps (as we should) for the --suggest option and the 1.2 branch extended on that concept that we scale steps already as early as reading them. The development release of SPARK fixed the distinction between raw and scaled steps in the JSON output (i.e. check_tree vs. stats object).

Expected Behavior
To prepare for future releases of SPARK, SPAT should be able to detect if step scaling is actually needed and skip the scaling if not. If there is at least one successful proof, we can infer that information from the difference of reported steps in the check_tree array and the corresponding stats object.
Alternatively, we may provide a command line switch to enable scaling or not.

Invalid output of --suggest option

Describe the bug
The output of the --suggest option contains too many quotes after the --steps option.

Console Output

Warning: You requested a suggested prover configuration.
Warning: This feature is highly experimental.
Warning: Please consult the documentation.

package Prove is
   for Prover_Switches ("sparknacl-car.adb") use ("--provers=CVC4", "--steps=5882"", "--timeout=1");

GNAT2020 compatibility

Format of the .spark files seems slightly changed in the GNAT2020 release. See what the differences are and solve these in a preferably backward compatible way.

Sorting by successful proof time should not intermix with unproved items

Describe the bug
As mentioned in the README, reports sorted by successful proof time (i.e. -cs) also show unproved items interspersed with proved items. I am assuming that if a user wants to see the times for successful proofs, unproved VCs are currently irrelevant, so they should be shown last.

Provide --cut-off command line parameter

Is your feature request related to a problem? Please describe.

After fixing #22 I noticed that it's a bit useless to suddenly show all proofs with a time of 0.0 s (tool limitation).

Describe the solution you'd like
We should provide a command line parameter (I propose --cut-off) which suppresses output for entities whose proof times are below that.

Additional context
Also, vaguely related to #1.

Need to install GNATColl on FSF CI chain

Describe the bug
WIth the FSF target, GNATColl is not available by default. We need to install it first.

Emit warning if proof times do not match?

While #22 is now documented under tool limitations it could be nice to issue a warning to the user if such data is encountered (i.e. the times reported in the file and the summed proof times vastly differ and most proof times are 0.0 s).

Describe the solution you'd like
Emit a text like "Warning: Data seems to be from a non-pristine run, timing results will be inaccurate." to notify the user of the issue.

Additional context
If the tool is used in "iterative proof mode" (see README), the additional warning may be more disturbing than helpful.
Making the warning optional is pointless (as the user would actively need to enable it), forcing the user to say they do not want such warnings on each run could be annoying, too...

Show steps for successful proof

Is your feature request related to a problem? Please describe.
While reducing --timeout to improve the proof time is a valid option, it is not very reliable when GNATprove is executed on machines with very different computing power. A reproducible proof setting is especially important when GNATprove is regularly run on external machines with unknown resources (e.g., a CI provider). That is why I usually prefer to use --steps instead (or in combination with a high timeout). Unfortunately, SPAT doesn't analyze proof steps.

Describe the solution you'd like
The steps could be shown along with the time. For example:

RFLX.RFLX_Types.U64_Insert => 120.0 s/1.6 ks 87391 steps
`-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 120.0 s/491.0 s 46034 steps
  -altergo: 188.2 ms 46034 steps (Valid)
[...]

It should be also possible to sort the output by the number of steps, so that the most difficult units of the whole project can be easily seen.

`spat.py` likely to be too strict about matching filenames

Describe the bug
The regular expression for a file:line:column "([a-z0-9-]+\.ad[bs]):(\d+):(\d+)" only works if the standard GNAT convention is used, as soon as there are upper case letters, it won't match, so spat.py will not show anything.

Also, the original expression totally missed that we could have underscores in file names.

Document compilation

Hello,

Unless I missed it, the project doesn't contain any info to build the executable. I tried

$ gprbuild -P spat
spat.gpr:2:06: unknown project file: "si_units_lib"
gprbuild: "spat" processing failed

I discovered the SI_Units project in your github profile, so I will go download that now ...

Let the tool suggest an "optimal" prover configuration.

Is your feature request related to a problem? Please describe.
A lot of times, optimizing proof times just consists of shuffling around which prover should be called first.
See, for example this PR

Describe the solution you'd like
Given the data provided, the tool should output a suggested configuration of prover/file matrix.

Describe alternatives you've considered
Manually reading through the output. But well, we do have a tool, we do have the data, so why not use both?

--details option sometimes seem too detailed

Is your feature request related to a problem? Please describe.
When a single entity has a lot of verification conditions and paths leading to them, showing all of these is sometimes just too much information.

Describe the solution you'd like
The --details option could be enhanced with a "level", e.g. --details=1 shows only the first level (the VC), while --details=2 would also show the proof paths.

This probably would be most useful in conjunction with #34.

Show max/success steps also in summary and less detailed report modes

Is your feature request related to a problem? Please describe.

See latest comments on issue #30.

Describe the solution you'd like

• Steps should also be shown in summary and report mode without details (although I suspect, we should show the scaled steps then, not the prover specific raw ones which are currently shown in the detailed modes).

• Also, sorting by (scaled) steps should be possible.

Suggested steps too low

Describe the bug
The suggested steps are in some cases too low for a successful proof. While 1672 steps are suggested, 1768 steps are required.

$ run_spat -Ptest.gpr --suggest
[...]
package Prove is
   for Proof_Switches ("rflx-arrays-tests.adb") use ("--prover=Z3", "--steps=1672", "--timeout=1");
end Prove;

$ sparkprof -Ptest -u rflx-arrays-tests
---------------------------------------------------------------------------------------
UNIT                                                  MAX STEPS    MAX TIME  TOTAL TIME
[...]
rflx-arrays-tests                                       1768 steps     0.0 s     0.0 s

Here is the relevant .spark file: rflx-arrays-tests.spark.txt

Used version: run_spat V1.1.3 (compiled by SYSTEM_NAME_GNAT Community 2020 (20200429-93))

Suggested configuration leads to failing proof

Describe the bug
The --suggest option has multiple issues:

1. The determined steps seem to be wrong. In my example they were either too high or too low.
2. The determined timeout is too low.
3. Setting --steps and --timeout using Prover_Switches has no effect.

To Reproduce
So far I'm using sparkprof to determine the maximum number of steps. Here is an example (the two used files can be found here):

$ sparkprof -Ptest --level=4
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
------------------------------------------------------
UNIT                 MAX STEPS    MAX TIME  TOTAL TIME
rflx-rflx_arithmetic  90761 steps    21.0 s    54.2 s
ALL                   90761 steps    21.0 s    54.2 s

Based on that output I would add the following to the project file:

   package Prove is
      for Proof_Switches ("rflx-rflx_arithmetic.ads") use ("--steps=90761");
      for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--steps=90761");
   end Prove;

After adding these switches to the project the project can still be proven. If the steps value is changed to 90760, gnatprove fails as expected.

SPAT suggests quite different options:

package Prove is
   for Prover_Switches ("rflx-rflx_arithmetic.adb") use ("--provers=CVC4", "--steps=82085", "--timeout=1");
   for Prover_Switches ("rflx-rflx_arithmetic.ads") use ("--provers=CVC4", "--steps=3191607", "--timeout=21");
end Prove;

When I use the proposed switches, gnatprove fails:

$ gnatprove -Ptest               
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
rflx-rflx_arithmetic.adb:11:13: medium: divide by zero might fail [possible explanation: precondition of subprogram at rflx-rflx_arithmetic.ads:16 should mention Value]
[...]

This seems to have multiple reasons:

• --steps and --timeout seem to be ignored in Prover_Switches. They have an effect as soon as I replace Prover_Switches by Proof_Switches (and remove --provers).
• The timeout seems to be to low. Many failing checks vanish when --timeout is removed.
• The suggested steps for rflx-rflx_arithmetic.adb are too low. The remaining failing check vanishes when the steps are increased to 90761.

Number of steps may exceed range of Natural

Describe the bug
See #29 (comment)

Current suspicion is that the reported number of steps exceeds the 2**31 mark (i.e. > Natural'Last). Steps should be recorded in a 64 bit integer.

Expected Behavior
Not a Constraint_Error.

Fix spurious warnings

For SPARK CE 2020, we spit out warnings that an (empty) check_tree is not a JSON array, because with the 2020 file format, an empty JSON object appears there instead of the expected array (i.e. [] vs. {}).

We should probably relax this check, i.e. this requires warning-less Preconditions.

Incorrect warning about missing timings

When running SPAT on a toy project, I get warnings like these:

Warning: Expected field "gnatwhy3.run_vcs" not present!
Warning: Expected field "gnatwhy3.register_vcs" not present!
Warning: Expected field "gnatwhy3.schedule_vcs" not present!

But it's expected to have such missing fields, it just means the corresponding phase wasn't run at all. For the statistics, the tool should assume the phase took no time (0s).

Show unjustified proofs

Right now, unproven VCs are all shown regardless if they have a justification message or not. We should add a --unjustified command line parameter which would work in conjunction with the --unproved parameter to only show unproven VCs with no associated justification.