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

**URL:** <https://forum.ada-lang.io/t/how-does-gnatprove-flow-debug-use-graphviz/1067>\
**Category:** General\
**Tags:** spark\
**Created:** [August 10, 2024, 6:19pm UTC](https://forum.ada-lang.io/t/how-does-gnatprove-flow-debug-use-graphviz/1067 "2024-08-10T18:19:56Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![mgrojo](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/mgrojo/32/15_2.png) [@mgrojo](https://forum.ada-lang.io/u/mgrojo)\
**Post date:** [August 10, 2024, 6:19pm UTC](https://forum.ada-lang.io/t/how-does-gnatprove-flow-debug-use-graphviz/1067/1 "2024-08-10T18:19:56Z")

</div>

I saw this switch for `gnatprove`

```term
 --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?

---

<div class="post-metadata">

**Author:** ![Irvise](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/i/7ba0ec/32.png) [@Irvise](https://forum.ada-lang.io/u/Irvise)\
**Post date:** [August 11, 2024, 8:55am UTC](https://forum.ada-lang.io/t/how-does-gnatprove-flow-debug-use-graphviz/1067/2 "2024-08-11T08:55:30Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![OPi](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/opi/32/31_2.png) [@OPi](https://forum.ada-lang.io/u/OPi)\
**Post date:** [August 11, 2024, 9:54am UTC](https://forum.ada-lang.io/t/how-does-gnatprove-flow-debug-use-graphviz/1067/3 "2024-08-11T09:54:16Z")

</div>

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

> **[GitHub - jrfonseca/xdot.py: Interactive viewer for graphs written in...](https://github.com/jrfonseca/xdot.py)**
>
> Interactive viewer for graphs written in Graphviz's dot language.

(But Graphviz and some other tools are needed.)

---

<div class="post-metadata">

**Author:** ![mgrojo](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/mgrojo/32/15_2.png) [@mgrojo](https://forum.ada-lang.io/u/mgrojo)\
**Post date:** [August 11, 2024, 11:29am UTC](https://forum.ada-lang.io/t/how-does-gnatprove-flow-debug-use-graphviz/1067/4 "2024-08-11T11:29:52Z")

</div>

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.