[klee-dev] A strange STP expression generated

[Qiuping Yi]

Hi, everybody,

Now I encountered a strange thing, and I need your help.

When I resolve stp to query the next result of the next expression from
KLEE,

(Eq false
    (Slt 0
         (ReadLSB w32 0 const_arr10)))

It told me that it is unsolvable, and I printed the expression in stp with
command *vc_printVarDecls(vc)* and *vc_printExpr(vc, e)*,
then it represented:

__tmpInt8  : BITVECTOR(8);
__tmpInt16  : BITVECTOR(16);
__tmpInt32  : BITVECTOR(32);
__tmpInt64  : BITVECTOR(64);
x_0x2d4edf0  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
y_0x2d4f560  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
z_0x2d45900  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
const_arr10_0x2d9d810  : ARRAY BITVECTOR(32) OF BITVECTOR(8); // var
declaration
*(LET let_k_0 = ((((const_arr10_0x2d9d810 WITH [0x00000000] := 0x00)*
* WITH [0x00000001] := 0x00)*
* WITH [0x00000002] := 0x00)*
* WITH [0x00000003] := 0x00)*
* IN *
( NOT( SBVLT(0x00000000,(let_k_0[0x00000003] @ (let_k_0[0x00000002] @
(let_k_0[0x00000001] @ let_k_0[0x00000000]
)
)
))
)))

Could you tell me what does the bold part mean?? I think only the red part
is needed for represent this expression.

In addition, when I query the next KLEE expression,

(Eq false
    (Slt 0
         (ReadLSB w32 0 x)))

the related stp expression just is:

( NOT( SBVLT(0x00000000,(x_0x2d4edf0[0x00000003] @ (x_0x2d4edf0[0x00000002]
@ (x_0x2d4edf0[0x00000001] @ x_0x2d4edf0[0x00000000]
)
)
))
))

SO, what's wrong? How can I query the result of the first expression with
STP?

Thank you all in advance.

--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
-------------- next part --------------
HTML attachment scrubbed and removed