GDB с Emacs и F*

Я хотел бы отладить простую F* программу, используя Emacs fstar-mode и gdb. В самом конце вики режима fstar https://github.com/FStarLang/fstar-mode.el есть информация:

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

без дальнейших объяснений.

Когда в Emacs (допустим, я редактирую файл Test.fst), я вызываю fstar-gdb командовать и перейти к gdb консоль я пытаюсь использовать команды file Test а также run, Они работают правильно, однако break 3 (или любая другая строка) говорит, что не удалось найти строку 3 в main.c (Очевидно).

Как я использую gdb с F*?

Источник

1 ответ

Решение

Команда fstar-gdb предназначена для самого отладчика F*, а не для программ, скомпилированных с F*.

Для программ F* лучше всего будет:

  • ocamldebug, если вы используете байт-компилятор
  • обычная процедура отладки программ OCaml в GDB (см. https://ocaml.org/meetings/ocaml/2012/slides/oud2012-paper5-slides.pdf; это потому, что большинство программ F* перед компиляцией извлекаются в OCaml),
  • обычная процедура отладки GDB-программ на C, если вы используете Low*.
Источник
Другие вопросы по тегам