代码之家 › 专栏 › 技术社区 › Bartek Wójcik

带Emacs和f的gdb*

fstar-mode fstar gdb emacs

1

Bartek Wójcik · 技术社区 · 7 年前

我想使用emacs fstar模式和gdb调试简单的f*程序。在fstar模式的wiki的最末端 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 (或任何其他行)说在 main.c (显然)。

如何使用 GDB 用f*?

1 回复 | 直到 7 年前

1

Clément 7 年前

fstar gdb命令用于调试f*编译器本身,而不是用f*编译的程序。

对于F*项目,最好的可能是:

如果使用字节编译器,则使用ocamldebug
OCAML程序的gdb调试的常规过程(参见 https://ocaml.org/meetings/ocaml/2012/slides/oud2012-paper5-slides.pdf ;这是因为大多数f*程序在编译之前都被提取到ocaml中)。
如果使用的是low*,调试C程序gdb调试的常规过程。