Gdb与经济、社会和文化事务部和法*

Question

我想用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中找不到第3行(很明显)。

如何在F*中使用gdb？

Answer 1

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

就F*方案而言，最好的办法是：

• 如果使用字节编译器，则使用using调试。
• GDB调试OCaml程序的通常过程(请参阅https://ocaml.org/meetings/ocaml/2012/slides/oud2012-paper5-slides.pdf；这是因为大多数F*程序在编译前被解压缩到OCaml )。
• 调试GDB调试C程序的通常过程，如果您使用的是Low*。