[K-Bug] Setting subject in debugging

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.

Reproduce the issue with kompile lesson-19-a.k --enable-llvm-debug and krun -cPGM=0 --debugger, then inspect the k_step location shown at line 287 of lesson-02-a.k. Compare the debugger output with the tutorial’s expected <k> subject and check help k; done means the documented debugging flow shows the expected subject or clearly explains how to change it.