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*?
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: