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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
