The error can be caused by an inline asm instruction in your program
(e.g. call i32 asm ...). KLEE does not support them.
Paul
On 21/02/12 09:46, Jiaqi Tan wrote:
> 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
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
