[klee-dev] A strange STP expression generated

[Cristian Cadar]

Hi,

The two expressions are indeed not equivalent, you seem to be printing 
different things in CVC and Kleaver formats.  You can use 
--use-query-log=all:pc to print out the entire set of queries issued by 
KLEE, using its own query language.

Cristian

On 06/10/14 05:54, Qiuping Yi wrote:
> 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
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>