How does `gnatprove --flow-debug` use graphviz?

General
1

I saw this switch for gnatprove

 --flow-debug         Extra debugging for flow analysis (requires graphviz)

and I expected it to generate some kind of graph of the dependencies in the graphviz format, or a direct call to one of the graphviz programs to directly generate the graph in an image.

But this is all what I got:

$ gnatprove -P contactos.gpr --flow-debug contactos.adb
Phase 1 of 2: generation of Global contracts ...
marking                                                        0.1s
Global generation (cons) of KIND_SUBPROGRAM inicializar
   skipped(global found)
   Spec in SPARK: yes
   Body in SPARK: yes
Global generation (cons) of KIND_SUBPROGRAM agregar_contacto
   skipped(global found)
   Spec in SPARK: yes
   Body in SPARK: yes
Global generation (cons) of KIND_PACKAGE contactos
   Spec in SPARK: yes
   Body in SPARK: yes
Global generation complete for current CU
globals (partial)                                              0.5s
Phase 2 of 2: flow analysis and proof ...
/home/mgr/.alire/libexec/spark/bin/why3server -j 1 --socket /tmp/why3server3733458521.sock --logging
globals (basic)                                                0.0s
globals (advanced)                                             0.1s
marking                                                        0.0s
properties (advanced)                                          0.0s
Flow analysis (cons) of KIND_SUBPROGRAM inicializar
   Spec_Scope: inicializar|spec
      contactos|spec
   Body_Scope: inicializar|body
Flow analysis (cons) of KIND_SUBPROGRAM agregar_contacto
   Spec_Scope: agregar_contacto|spec
      contactos|spec
   Body_Scope: agregar_contacto|body
Flow analysis (cons) of KIND_PACKAGE contactos
   Spec_Scope: contactos|spec
   Body_Scope: contactos|body
Flow analysis (errors) for KIND_SUBPROGRAM agregar_contacto
Flow analysis (errors) for KIND_PACKAGE contactos
Flow analysis (errors) for KIND_SUBPROGRAM inicializar
Flow analysis complete for current CU
flow analysis                                                  0.5s
codepeer results                                               0.0s
init_why_sections                                              0.0s
translation of standard                                        0.0s
gnatwhy3 --timeout 0 --steps 100 --memlimit 0 --prover cvc4 --proof per_check --socket /tmp/why3server3733458521.sock --debug -j 1 --counterexample off --giant-step-rac off --debug-why3 vc:do_not_keep_trace --warn-prover cvc4 --ce-timeout 10 /home/mgr/Documentos/universidad/uned/5. Trabajo Fin de Master/Memoria/obj/gnatprove/contactos__agregar_contacto.gnat-json 
gnatwhy3.run_vcs                                               0.0s
gnatwhy3.register_vcs                                          0.0s
gnatwhy3.schedule_vcs                                          0.0s
gnatwhy3.init                                                  0.5s
gnatwhy3.save_session                                          0.0s
VERDICT	NOT_CHECKED	Counterexample checking not requested	RES_NOT_EXECUTEDRES_NOT_EXECUTED	No giant-step result	contactos.adb:54:76
VERDICT	NOT_CHECKED	Counterexample checking not requested	RES_NOT_EXECUTEDRES_NOT_EXECUTED	No giant-step result	contactos.adb:54:64
VERDICT	NOT_CHECKED	Counterexample checking not requested	RES_NOT_EXECUTEDRES_NOT_EXECUTED	No giant-step result	contactos.adb:54:24
VERDICT	NOT_CHECKED	Counterexample checking not requested	RES_NOT_EXECUTEDRES_NOT_EXECUTED	No giant-step result	contactos.adb:54:73
Summary logged in [...]/gnatprove/gnatprove.out

Graphviz package is installed and dot and similar programs are visible in the path. Why is graphviz a dependency? Is it really used?

2

Hi,

I ran gnatprove -Pdefault.gpr --flow-debug with the WolfSSL/Ada binding and it generated quite a few .dot files in the obj/gnatprove directory. It seems there is one for each unit, but I may be wrong here, one such example is the file wolfssl_constants_2.dot. I found the directory as it is the same as the rest of the output, where gnatprove.out exists. See the last line of your log in your message.

One can turn the .dot file into a PDF (or other formats) using the following command dot -Tpdf obj/gnatprove/wolfssl_visibility_2.dot -o something.pdf

I hope this helps. Best regards,
Fer

1 Like
3

There is also this useful tool to view .dot files directly:

(But Graphviz and some other tools are needed.)

4

Oh, you’re right. I even have the PDF files there, and I haven’t generated them, so it seems gnatprove also generates the PDF if the Graphviz tools are available.

This is very hidden, I’d say this should be documented in the user guide, the switch help or, at least, in the tool output when generating the files.