search

HeisenbugLtd / spat

SPARK Proof Analysis Tool
https://github.heisenbug.eu/spat/
Do What The F*ck You Want To Public License
15 stars 4 forks source link

Suggested configuration is incomplete #55

Closed treiher closed 4 years ago

treiher commented 4 years ago

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)
  1. 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;
Jellix commented 4 years ago

Thanks for the report.

I think I understand the underlying issue. From the looks of it, the crudely implemented logic to figure out the proper source file name is especially broken when the .spark file references an entity from a generic unit: In such a case the name of the generic unit wins and as you can have multiple instantiations, they will be referenced more than once, forgetting about the actual name of the instantiation.

Jellix commented 4 years ago

Ok, I just released v1.1.2 which should fix the issue according to what I could test without my machine constantly crashing due to overheating. :)

treiher commented 4 years ago

Many thanks for your work. Unfortunately, I'm still not able to successfully prove the project with the suggested configuration. To narrow the problem down I reused the example used in #50. The suggested configuration for this example with version 1.1.2 is:

package Prove is
   for Proof_Switches ("rflx-rflx_arithmetic.ads") use ("--prover=CVC4", "--steps=90761", "--timeout=22");
end Prove;

Using that configuration leads to multiple failing checks:

$ 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]
rflx-rflx_arithmetic.adb:21:08: medium: postcondition might fail, cannot prove X / Pow2 (K) < Pow2 (J - K)
rflx-rflx_arithmetic.adb:21:10: medium: divide by zero might fail
rflx-rflx_arithmetic.adb:36:14: medium: postcondition might fail, cannot prove X * Pow2 (K) <= Pow2 (J + K) - Pow2 (K) (e.g. when J = 0 and K = 0 and X = 4611686018427387904)
rflx-rflx_arithmetic.adb:36:16: medium: overflow check might fail (e.g. when K = 0 and X = 12797496590450976783)
rflx-rflx_arithmetic.adb:36:43: medium: overflow check might fail
rflx-rflx_arithmetic.adb:37:16: medium: overflow check might fail (e.g. when K = 0 and X = 12797496590450976783)
rflx-rflx_arithmetic.adb:37:50: medium: overflow check might fail
rflx-rflx_arithmetic.adb:46:38: medium: divide by zero might fail
rflx-rflx_arithmetic.adb:54:38: medium: overflow check might fail (e.g. when Length = 0 and Result = 12797496590450976783 and Value = 12797496590450976783)
rflx-rflx_arithmetic.ads:20:08: medium: postcondition might fail, cannot prove Mod_Pow2'Result < 2**Exp
rflx-rflx_arithmetic.ads:30:08: medium: postcondition might fail, cannot prove Right_Shift'Result < 2**(Value_Size - Length)
rflx-rflx_arithmetic.ads:42:11: medium: postcondition might fail, cannot prove Left_Shift'Result <= Pow2 (Value_Size + Length) - Pow2 (Length) (e.g. when Left_Shift'Result = 0 and Length = 0)
rflx-rflx_arithmetic.ads:45:57: medium: overflow check might fail

I was able to solve that problem by specifying switches for rflx-rflx_arithmetic.adb instead of rflx-rflx_arithmetic.ads. It seems switches should be preferably specified for the body and not the specification.

Jellix commented 4 years ago

Interesting, considering that certain representatives of the tool chain developers said that it only considers a single unit.

So from what I understood, it shouldn't matter, which file is specified as long as there's one (and preferably only one). With that assumption, I obviously opted for the spec.

Well, at least that one is easy enough to fix.

Jellix commented 4 years ago

Alright, fixed in v1.1.3, which now prefers the bodies instead of specs.