Hi,

I did some poking around the KLEE source, and found that this error is
being generated due to the assertion here (code segment included):

===== begin code =====
const Cell& Executor::eval(KInstruction *ki, unsigned index,
                           ExecutionState &state) const {
  assert(index < ki->inst->getNumOperands());
  int vnumber = ki->operands[index];

  if (vnumber == -1) {
          std::cout << "Assert about to fail: #operands:" <<
ki->inst->getNumOperands() << " index:" << index << " vnumber:" <<
vnumber << std::endl;
  }

  assert(vnumber != -1 &&
         "Invalid operand to eval(), not a value or constant!");
===== end code =====

I suppose -1 is used as a special flag value here? Because later on,
(- vnumber - 2) is used to grab a constant 3 lines down in the code.
What does the operands array in KInstruction store, and where is it
populated?

Thanks!
Jiaqi

On Mon, Feb 20, 2012 at 1:52 PM, Jiaqi Tan <[email protected]> wrote:
> Hi,
>
> I'm trying to run BusyBox, and I'm getting this error message:
>
> KLEE: WARNING: executable has module level assembly (ignoring)
> KLEE: WARNING: calling external: syscall(54, 0, 21505, 231590832)
> KLEE: WARNING: calling __user_main with extra arguments.
> KLEE: WARNING: calling external: __xstat64(3, 231196304, 231603064)
> klee: Executor.cpp:1001: const klee::Cell&
> klee::Executor::eval(klee::KInstruction*, unsigned int,
> klee::ExecutionState&) const: Assertion `vnumber != -1 && "Invalid
> operand to eval(), not a value or constant!"' failed.
> 0  klee 0x089a79f8
> Aborted
>
> Does anybody have any idea where the source of the problem might be?
> I'm not quite sure where to get started to figure out where the
> problem is. Is this due to a compilation or linking problem due to
> missing code or libraries?
>
> Thanks!
> Jiaqi Tan
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev

Reply via email to