[klee-dev] KLEE 2.2 released

[Cristian Cadar]

Dear all,

KLEE 2.2 is now released, many thanks for all the great contributions!

And extra thanks to my co-maintainer @MartinNowack and to the authors of 
key improvements this release: @corrodedHash, @futile, @jbuening, @251, 
@kren1, @MartinNowack.


The full list of changes can be found at
https://github.com/klee/klee/releases/tag/v2.2

Best,
Cristian

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[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 path_set;
std::set func_set;
……
void Executor::stepInstruction(ExecutionState ) {
  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.


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev