[klee-dev] See llvm-ir
Nowack, Martin
m.nowack at imperial.ac.uk
Tue Jun 30 17:25:25 BST 2020
Hi,
There is currently no real option that does generate test0000.ll.
But you can workaround with the following option:
`-debug-print-instructions=`
Here the excerpt of the help output
--debug-print-instructions=<value> - Log instructions during execution.
=all:stderr - Log all instructions to stderr in format [src, inst_id, llvm_inst]
=src:stderr - Log all instructions to stderr in format [src, inst_id]
=compact:stderr - Log all instructions to stderr in format [inst_id]
=all:file - Log all instructions to file instructions.txt in format [src, inst_id, llvm_inst]
=src:file - Log all instructions to file instructions.txt in format [src, inst_id]
=compact:file - Log all instructions to file instructions.txt in format [inst_id]
For you the option should be: `=all:file` or `=compact:file` combined with
```
--debug-compress-instructions - Compress the logged instructions in gzip format (default=false).
```
After that you just use each line and split it. As example the following line (=all:):
```
libc/string/memset.c:27 2:3226:1: br label %9, !dbg !1210, !llvm.loop !1218
```
[src:src_line src_col:assembly.ll-line:path-id: llvm inst]
Hope that helps,
Martin
> On 30. Jun 2020, at 16:53, Yugesh Kothari <kothariyugesh at gmail.com> wrote:
>
> Hi,
>
> When I run KLEE, the llvm-ir (.ll) file is saved as assembly.ll
> However I would like to see the llvm instructions that Klee runs on for each call-path or trace of the program (like if there are 3 program paths that klee explores then I would like to get test00000.ll, test00001.ll, test00002.ll or something along those lines)
>
> Is there a flag to get this information?
>
> Thanks!
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
More information about the klee-dev
mailing list