I recently has a project to do with using replay ktests with KLEE.

The context is to use KLEE functionalities in eBPF programs such as traffic control and firewall.
I was able to compile .bc file, generate ktests based on this .bc file and also compile a .bin executable.

Now I’m using commands such as:
KTEST_FILE=test000001.ktest ../fw.bin -d ../tmp_results
to run the ktest file with binary.

Now it’s getting troubles, currently the problem is object name mismatch, reporting error messages:
KLEE_RUN_TEST_ERROR: object name mismatch. Requesting “output_port” but returning “user_buf”

what I can offer you is the name of maps used in the source code and lines of code where klee_make_symbolic is used.
` BPF_MAP_INIT(&tx_port, “tx_devices_map”, “”, “tx_device”);
BPF_MAP_INIT(&flow_ctx_table, “flowtable”, “pkt.flow”, “output_port”);

klee_make_symbolic(pkt, sizeof(struct pkt), “user_buf”);
klee_make_symbolic(&(temp), sizeof(temp), “VIGOR_DEVICE”);
`

My question is, by reading the definition of klee_make_symbolic in runtime/Runtest/intrinsic.c, there is no reason for output_port to be passed in.

This is in Ubuntu 22.04, klee 3.0 and LLVM 12.0.1.