[klee-dev] Some confusing results.

[Tuo Li]

Hello!
I am not very familiar with klee and I have gotten some confusing results.
I want to know which files and which functions are analyzed, so I add some codes to klee/lib/Core/Executor.cpp.
……
std::set<std::string> path_set;
std::set<std::string> func_set;
……
void Executor::stepInstruction(ExecutionState &state) {
  printDebugInstructions(state);
  if (statsTracker)
    statsTracker->stepInstruction(state);

  ++stats::instructions;
  ++state.steppedInstructions;
  state.prevPC = state.pc;
  Instruction *inst = state.pc.operator->()->inst;
  auto dl = inst->getDebugLoc();
  if (dl.get() != nullptr) {
    auto full_path = dl.get()->getFilename();
    if (path_set.find(full_path) == path_set.end() &&
                    full_path.str().find("runtime") == std::string::npos) {
        std::cout << full_path.str() << std::endl;
        path_set.insert(full_path);
    }
    if (full_path.str().find("runtime") == std::string::npos) {
        Function *func = inst->getParent()->getParent();
        if (func != NULL) {
            std::string func_name = func->getName().str();
            if (func_set.find(func_name) == func_set.end()) {
                std::cout << func_name;
                std::cout << " in ";
                std::cout << full_path.str() << std::endl;
                func_set.insert(func_name);
            }
        }
    }
  }
  ++state.pc;
  if (stats::instructions == MaxInstructions)
    haltExecution = true;
}

I run klee -posix-runtime zephyr.elf.bc -sym-arg 20, but only two files and two functions are printed by the above code.
Also, a bug “out of bound pointer” is reported. I wonder what does “out of bound pointer” means? It seems that several kinds of bugs such as NULL-pointer-dereference and buffer-overflow can be reported as “out of bound”.

Sincerely,
Tuo Li.


-------------- next part --------------
HTML attachment scrubbed and removed