Gdb with emacs and F*

Question

I would like to debug simple F* program using Emacs fstar-mode and gdb. At the very end of the wiki of fstar-mode https://github.com/FStarLang/fstar-mode.el is information:

The fstar-gdb command (M-x) attaches GDB to the current F* process and launches Emacs' GDB-mi interface

with no further explanation.

When in Emacs (lets assume I am editing Test.fst file) I invoke fstar-gdb command and proceed to gdb console I am trying to use commands file Test and run. They are working correctly, however break 3 (or any other line) says that it failed to find line 3 in main.c (obviously).

How do I use gdb with F*?

Let's narrow down where the error occurs. If you run gdb from a shell window instead of emacs, do you still get the error when you type `break 3`? — Mark Plotnick, Jan 21 '19 at 18:53
Unfortunately the output is: `(gdb) break 3 >>> Breakpoint 1 at 0x5555555c6790: file main.c, line 3. (gdb) run >>> Starting program: /home/kicjow/Desktop/msc-neuralnet-verification/fstar-test/Test.exe Breakpoint 1, main (argc=1, argv=0x7fffffffddb8) at main.c:32 32 main.c: No such file or directory. ` — Bartek Wójcik, Jan 21 '19 at 19:48

score 2 · Accepted Answer · answered Jan 22 '19 at 15:45

The fstar-gdb command is intended to the debug F* compiler itself, not programs compiled with F*.

For F* programs, the best would likely be:

ocamldebug if you're using the byte-compiler
the usual procedure for GDB debugging of OCaml programs (see https://ocaml.org/meetings/ocaml/2012/slides/oud2012-paper5-slides.pdf; this is because most F* programs are extracted to OCaml before being compiled).
the usual procedure for debugging GDB debugging of C programs if you're using Low*.

Gdb with emacs and F*

1 Answers1