Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Many warnings and void output for gnatprove from the Alire community index #68

Open
mgrojo opened this issue Feb 22, 2025 · 0 comments
Open
Assignees
Labels
bug Something isn't working

Comments

@mgrojo
Copy link

mgrojo commented Feb 22, 2025

Describe the bug
The only output with most of the switches are warnings.

To Reproduce
Steps to reproduce the behavior:

alr get vaton
cd vaton_*/
alr build
alr gnatprove
alr exec -P -- run_spat -s

Expected Behavior
Output like the examples in the documentation.

Console Output
If applicable, add output log from the tool, preferably with the --verbose option enabled.

Debug: GNAT project loaded in 73.2 ms.
Debug: Found "spark_unbound-arrays.adb"...Debug: "spark_unbound-arrays.spark" added to index.
Debug: Found "spark_unbound-arrays.ads"...Debug: "spark_unbound-arrays.spark" already in index.
Debug: Found "spark_unbound-safe_alloc.adb"...Debug: "spark_unbound-safe_alloc.spark" added to index.
Debug: Found "spark_unbound-safe_alloc.ads"...Debug: "spark_unbound-safe_alloc.spark" already in index.
Debug: Found "spark_unbound.ads"...Debug: "spark_unbound.spark" added to index.
Debug: Found "vaton_config.ads"...Debug: "vaton_config.spark" added to index.
Debug: Found "vaton-float_conversions.adb"...Debug: "vaton-float_conversions.spark" added to index.
Debug: Found "vaton-float_conversions.ads"...Debug: "vaton-float_conversions.spark" already in index.
Debug: Found "vaton-integer_conversions.adb"...Debug: "vaton-integer_conversions.spark" added to index.
Debug: Found "vaton-integer_conversions.ads"...Debug: "vaton-integer_conversions.spark" already in index.
Debug: Found "vaton.adb"...Debug: "vaton.spark" added to index.
Debug: Found "vaton.ads"...Debug: "vaton.spark" already in index.
Debug: Search completed in 829.2 µs, 7 files found.
Debug: Using up to 4 parsing threads.
Debug: Queuing "/home/mgr/.local/share/alire/builds/spark_unbound_0.2.1_1f8dae01/780397e81eb867a3309ee1c923c9564fb9400fd7e56bbee7390685b246f004ec/obj/gnatprove/spark_unbound.spark"...
Debug: Queuing "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton-integer_conversions.spark"...
Debug: Queuing "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton_config.spark"...
Debug: Queuing "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton-float_conversions.spark"...
Debug: Queuing "/home/mgr/.local/share/alire/builds/spark_unbound_0.2.1_1f8dae01/780397e81eb867a3309ee1c923c9564fb9400fd7e56bbee7390685b246f004ec/obj/gnatprove/spark_unbound-safe_alloc.spark"...
Debug: Queuing "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton.spark"...
Debug: Queuing "/home/mgr/.local/share/alire/builds/spark_unbound_0.2.1_1f8dae01/780397e81eb867a3309ee1c923c9564fb9400fd7e56bbee7390685b246f004ec/obj/gnatprove/spark_unbound-arrays.spark"...
Debug: Picking up results...
Debug: "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton_config.spark"...ok.
Debug: "/home/mgr/.local/share/alire/builds/spark_unbound_0.2.1_1f8dae01/780397e81eb867a3309ee1c923c9564fb9400fd7e56bbee7390685b246f004ec/obj/gnatprove/spark_unbound.spark"...ok.
Debug: "/home/mgr/.local/share/alire/builds/spark_unbound_0.2.1_1f8dae01/780397e81eb867a3309ee1c923c9564fb9400fd7e56bbee7390685b246f004ec/obj/gnatprove/spark_unbound-safe_alloc.spark"...ok.
Debug: "/home/mgr/.local/share/alire/builds/spark_unbound_0.2.1_1f8dae01/780397e81eb867a3309ee1c923c9564fb9400fd7e56bbee7390685b246f004ec/obj/gnatprove/spark_unbound-arrays.spark"...ok.
Debug: "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton-integer_conversions.spark"...ok.
Debug: "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton-float_conversions.spark"...ok.
Debug: "/home/mgr/src/alire/vaton_0.1.0_c07eed4c/obj/development/gnatprove/vaton.spark"...ok.
Debug: Parsing completed in 63.6 ms.
Debug: Detected file version of "spark_unbound.spark" is GNAT_CE_2020.
Warning: Field "spark" not of expected type "JSON_ARRAY_TYPE"!
Warning: Expected field "flow analysis" not present!
Debug: Detected file version of "vaton-integer_conversions.spark" is GNAT_CE_2020.
Warning: Field "spark" not of expected type "JSON_ARRAY_TYPE"!
Warning: Field "entity" not of expected type "JSON_OBJECT_TYPE"!
[Repeats many times]
Warning: Field "entity" not of expected type "JSON_OBJECT_TYPE"!
Warning: Expected field "flow analysis" not present!
Debug: Detected file version of "vaton_config.spark" is GNAT_CE_2020.
Warning: Field "spark" not of expected type "JSON_ARRAY_TYPE"!
Warning: Expected field "flow analysis" not present!
Debug: Detected file version of "vaton-float_conversions.spark" is GNAT_CE_2020.
Warning: Field "spark" not of expected type "JSON_ARRAY_TYPE"!
Warning: Field "entity" not of expected type "JSON_OBJECT_TYPE"!
[Repeats many times]
Warning: Field "entity" not of expected type "JSON_OBJECT_TYPE"!
Warning: Expected field "flow analysis" not present!
Debug: Detected file version of "spark_unbound-safe_alloc.spark" is GNAT_CE_2020.
Warning: Field "spark" not of expected type "JSON_ARRAY_TYPE"!
Warning: Expected field "flow analysis" not present!
Debug: Detected file version of "vaton.spark" is GNAT_CE_2020.
Warning: Field "spark" not of expected type "JSON_ARRAY_TYPE"!
Warning: Field "entity" not of expected type "JSON_OBJECT_TYPE"!
[Repeats many times]
Warning: Field "entity" not of expected type "JSON_OBJECT_TYPE"!
Warning: Expected field "flow analysis" not present!
Debug: Detected file version of "spark_unbound-arrays.spark" is GNAT_CE_2020.
Warning: Field "spark" not of expected type "JSON_ARRAY_TYPE"!
Warning: Expected field "flow" not present!
Warning: Expected field "proof" not present!
Warning: Expected field "flow analysis" not present!
Debug: Reading completed in 4.2 ms.
Debug: Collecting files completed in 141.9 ms.
Debug: Cut off point set to 0.0 s.
spark_unbound.spark             => (Flow  => 0.0 s,
                                    Proof => 0.0 s (0 steps)/0.0 s (0 steps)/0.0 s)
vaton-integer_conversions.spark => (Flow  => 0.0 s,
                                    Proof => 0.0 s (0 steps)/0.0 s (0 steps)/0.0 s)
vaton_config.spark              => (Flow  => 0.0 s,
                                    Proof => 0.0 s (0 steps)/0.0 s (0 steps)/0.0 s)
vaton-float_conversions.spark   => (Flow  => 0.0 s,
                                    Proof => 0.0 s (0 steps)/0.0 s (0 steps)/0.0 s)
spark_unbound-safe_alloc.spark  => (Flow  => 0.0 s,
                                    Proof => 0.0 s (0 steps)/0.0 s (0 steps)/0.0 s)
vaton.spark                     => (Flow  => 0.0 s,
                                    Proof => 0.0 s (0 steps)/0.0 s (0 steps)/0.0 s)
spark_unbound-arrays.spark      => (Flow  => 0.0 s,
                                    Proof => 0.0 s (0 steps)/0.0 s (0 steps)/0.0 s)

Additional Context
Is the tool maybe incompatible with the files produced by gnatprove from the Alire community (version 14.1.1).

@mgrojo mgrojo added the bug Something isn't working label Feb 22, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants