GDB с Emacs и F * - PullRequest
Новая
       11

GDB с Emacs и F *

0 голосов
/ 21 января 2019

Я бы хотел отладить простую F * программу, используя Emacs fstar-mode и gdb. В самом конце вики fstar-mode 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 Ответ

0 голосов
/ 22 января 2019

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

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

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