[K-Bug] Setting subject in debugging

[celine-celine]

What component is the issue in?

llvm-backend

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v6.1.98

Operating System

Linux

K Definitions (If Possible)

module LESSON-19-A
imports INT
rule I => I +Int 1
requires I <Int 100
endmodule

Steps to Reproduce

While going through lesson 1.19 in k tutorial, after running the kompile lesson-19-a.k --enable-llvm-debug and krun -cPGM=0 --debugger, it returns the following result as:

Temporary breakpoint 1 at 0x839e0
Starting program: /home/scarlett/k-tutorial/lesson-02-a-kompiled/interpreter /tmp/.krun-2024-03-13-21-49-58-HgvcekYO99/tmp.in.z6w0rpZ0Er -1 /tmp/.krun-2024-03-13-21-49-58-HgvcekYO99/result.kore
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Temporary breakpoint 1, 0x00005555555d79e0 in main ()
0x00005555555b9530 in k_step (subject=#Bottom) at /home/scarlett/k-tutorial/lesson-02-a.k:287
287     rule I => I +Int 1

Expected Results

According to the tutorial, subject here should be instead of #Bottom, however, it cannot be found either in the tutorial or in 'help k' about how to change subject.

[Baltoli]

Hi @celine-celine; thanks for your interest in K! The GDB support for K is currently broken; it's tricky code to maintain and test reliably, but fixing it is very much on our agenda. I'm going to triage this issue to the correct place to make sure that it gets logged alongside related issues.

For the time being, you can safely skip the GDB lesson and move on to the rest of the tutorial. Please let us know if there are any other issues you experience!